feat: synchronize with mathlib3 #16523

Mathlib/Algebra/GroupPower/Order.lean

@@ -370,7 +370,7 @@ theorem pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n
   | 0, hn => by contradiction
   | n + 1, _ => by
     simpa only [pow_succ'] using
-      mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
+      mul_lt_mul_of_le_of_ltₚ' (pow_le_pow_of_le_left hx h.le _) h hx (pow_pos (hx.trans_lt h) _)
 #align pow_lt_pow_of_lt_left pow_lt_pow_of_lt_left
 
 theorem strictMonoOn_pow (hn : 0 < n) : StrictMonoOn (fun x : R => x ^ n) (Set.Ici 0) :=

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -499,14 +499,6 @@ instance (priority := 100) StrictOrderedSemiring.toOrderedSemiring : OrderedSemi
       mul_le_mul_of_nonneg_right }
 #align strict_ordered_semiring.to_ordered_semiring StrictOrderedSemiring.toOrderedSemiring
 
-theorem mul_lt_mul (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) (hc : 0 ≤ c) : a * b < c * d :=
-  (mul_lt_mul_of_pos_right hac hb).trans_le <| mul_le_mul_of_nonneg_left hbd hc
-#align mul_lt_mul mul_lt_mul
-
-theorem mul_lt_mul' (hac : a ≤ c) (hbd : b < d) (hb : 0 ≤ b) (hc : 0 < c) : a * b < c * d :=
-  (mul_le_mul_of_nonneg_right hac hb).trans_lt <| mul_lt_mul_of_pos_left hbd hc
-#align mul_lt_mul' mul_lt_mul'
-
 @[simp]
 theorem pow_pos (H : 0 < a) : ∀ n : ℕ, 0 < a ^ n
   | 0 => by
@@ -537,10 +529,6 @@ protected theorem Decidable.mul_lt_mul'' [@DecidableRel α (· ≤ ·)] (h1 : a
     rw [← b0, mul_zero]; exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)
 #align decidable.mul_lt_mul'' Decidable.mul_lt_mul''
 
-theorem mul_lt_mul'' : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d := by classical
-  exact Decidable.mul_lt_mul''
-#align mul_lt_mul'' mul_lt_mul''
-
 theorem lt_mul_left (hn : 0 < a) (hm : 1 < b) : a < b * a := by
   convert mul_lt_mul_of_pos_right hm hn
   rw [one_mul]
@@ -786,14 +774,6 @@ theorem nonneg_of_mul_nonneg_right (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b :=
   le_of_not_gt fun hb => (mul_neg_of_pos_of_neg ha hb).not_le h
 #align nonneg_of_mul_nonneg_right nonneg_of_mul_nonneg_right
 
-theorem neg_of_mul_neg_left (h : a * b < 0) (hb : 0 ≤ b) : a < 0 :=
-  lt_of_not_ge fun ha => (mul_nonneg ha hb).not_lt h
-#align neg_of_mul_neg_left neg_of_mul_neg_left
-
-theorem neg_of_mul_neg_right (h : a * b < 0) (ha : 0 ≤ a) : b < 0 :=
-  lt_of_not_ge fun hb => (mul_nonneg ha hb).not_lt h
-#align neg_of_mul_neg_right neg_of_mul_neg_right
-
 theorem nonpos_of_mul_nonpos_left (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0 :=
   le_of_not_gt fun ha : a > 0 => (mul_pos ha hb).not_le h
 #align nonpos_of_mul_nonpos_left nonpos_of_mul_nonpos_left

Mathlib/Algebra/Order/Ring/Lemmas.lean

@@ -198,45 +198,82 @@ theorem mul_le_mul_left [PosMulMono α] [PosMulMonoRev α] (a0 : 0 < a) : a * b
 theorem mul_le_mul_right [MulPosMono α] [MulPosMonoRev α] (a0 : 0 < a) : b * a ≤ c * a ↔ b ≤ c :=
   @rel_iff_cov α>0 α (fun x y => y * x) (· ≤ ·) _ _ ⟨a, a0⟩ _ _
 
-theorem mul_lt_mul_of_pos_of_nonneg [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d)
-    (a0 : 0 < a) (d0 : 0 ≤ d) : a * c < b * d :=
+theorem mul_le_mul_of_le_of_leₚ [PosMulMono α] [MulPosMono α]
+    (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) : a * c ≤ b * d :=
+  (mul_le_mul_of_nonneg_left h₂ a0).trans (mul_le_mul_of_nonneg_right h₁ d0)
+
+theorem mul_le_mul_of_le_of_leₚ' [PosMulMono α] [MulPosMono α]
+    (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) : a * c ≤ b * d :=
+  (mul_le_mul_of_nonneg_right h₁ c0).trans (mul_le_mul_of_nonneg_left h₂ b0)
+
+theorem mul_lt_mul_of_le_of_ltₚ [PosMulStrictMono α] [MulPosMono α]
+    (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) : a * c < b * d :=
   (mul_lt_mul_of_pos_left h₂ a0).trans_le (mul_le_mul_of_nonneg_right h₁ d0)
 
-theorem mul_lt_mul_of_le_of_le' [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d)
-    (b0 : 0 < b) (c0 : 0 ≤ c) : a * c < b * d :=
+theorem mul_lt_mul_of_le_of_ltₚ' [PosMulStrictMono α] [MulPosMono α]
+    (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) : a * c < b * d :=
   (mul_le_mul_of_nonneg_right h₁ c0).trans_lt (mul_lt_mul_of_pos_left h₂ b0)
 
-theorem mul_lt_mul_of_nonneg_of_pos [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d)
-    (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d :=
+theorem mul_lt_mul_of_lt_of_leₚ [PosMulMono α] [MulPosStrictMono α]
+    (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d :=
   (mul_le_mul_of_nonneg_left h₂ a0).trans_lt (mul_lt_mul_of_pos_right h₁ d0)
 
-theorem mul_lt_mul_of_le_of_lt' [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d)
-    (b0 : 0 ≤ b) (c0 : 0 < c) : a * c < b * d :=
+theorem mul_lt_mul_of_lt_of_leₚ' [PosMulMono α] [MulPosStrictMono α]
+    (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) : a * c < b * d :=
   (mul_lt_mul_of_pos_right h₁ c0).trans_le (mul_le_mul_of_nonneg_left h₂ b0)
 
-theorem mul_lt_mul_of_pos_of_pos [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d)
-    (a0 : 0 < a) (d0 : 0 < d) : a * c < b * d :=
+theorem mul_lt_mul_of_lt_of_ltₚ [PosMulStrictMono α] [MulPosStrictMono α]
+    (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) : a * c < b * d :=
   (mul_lt_mul_of_pos_left h₂ a0).trans (mul_lt_mul_of_pos_right h₁ d0)
 
-theorem mul_lt_mul_of_lt_of_lt' [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d)
-    (b0 : 0 < b) (c0 : 0 < c) : a * c < b * d :=
+theorem mul_lt_mul_of_lt_of_ltₚ' [PosMulStrictMono α] [MulPosStrictMono α]
+    (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) : a * c < b * d :=
   (mul_lt_mul_of_pos_right h₁ c0).trans (mul_lt_mul_of_pos_left h₂ b0)
 
-theorem mul_lt_of_mul_lt_of_nonneg_left [PosMulMono α] (h : a * b < c) (hdb : d ≤ b) (ha : 0 ≤ a) :
-    a * d < c :=
-  (mul_le_mul_of_nonneg_left hdb ha).trans_lt h
+alias mul_le_mul_of_le_of_leₚ' ← mul_le_mul -- this name was in `Algebra.Order.Ring.Defs`
+alias mul_lt_mul_of_lt_of_leₚ' ← mul_lt_mul -- this name was in `Algebra.Order.Ring.Defs`
+alias mul_lt_mul_of_le_of_ltₚ' ← mul_lt_mul' -- this name was in `Algebra.Order.Ring.Defs`
+
+theorem mul_le_of_mul_le_leftₚ [PosMulMono α]
+    (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d ≤ c :=
+  (mul_le_mul_of_nonneg_left hle a0).trans h
+
+theorem mul_lt_of_mul_lt_leftₚ [PosMulMono α]
+    (h : a * b < c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d < c :=
+  (mul_le_mul_of_nonneg_left hle a0).trans_lt h
+
+theorem le_mul_of_le_mul_leftₚ [PosMulMono α]
+    (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a ≤ b * d :=
+  h.trans (mul_le_mul_of_nonneg_left hle b0)
+
+theorem lt_mul_of_lt_mul_leftₚ [PosMulMono α]
+    (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a < b * d :=
+  h.trans_le (mul_le_mul_of_nonneg_left hle b0)
+
+theorem mul_le_of_mul_le_rightₚ [MulPosMono α]
+    (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b ≤ c :=
+  (mul_le_mul_of_nonneg_right hle b0).trans h
+
+theorem mul_lt_of_mul_lt_rightₚ [MulPosMono α]
+    (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b < c :=
+  (mul_le_mul_of_nonneg_right hle b0).trans_lt h
 
-theorem lt_mul_of_lt_mul_of_nonneg_left [PosMulMono α] (h : a < b * c) (hcd : c ≤ d) (hb : 0 ≤ b) :
-    a < b * d :=
-  h.trans_le <| mul_le_mul_of_nonneg_left hcd hb
+theorem le_mul_of_le_mul_rightₚ [MulPosMono α]
+    (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a ≤ d * c :=
+  h.trans (mul_le_mul_of_nonneg_right hle c0)
 
-theorem mul_lt_of_mul_lt_of_nonneg_right [MulPosMono α] (h : a * b < c) (hda : d ≤ a) (hb : 0 ≤ b) :
-    d * b < c :=
-  (mul_le_mul_of_nonneg_right hda hb).trans_lt h
+theorem lt_mul_of_lt_mul_rightₚ [MulPosMono α]
+    (h : a < b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a < d * c :=
+  h.trans_le (mul_le_mul_of_nonneg_right hle c0)
 
-theorem lt_mul_of_lt_mul_of_nonneg_right [MulPosMono α] (h : a < b * c) (hbd : b ≤ d) (hc : 0 ≤ c) :
-    a < d * c :=
-  h.trans_le <| mul_le_mul_of_nonneg_right hbd hc
+alias mul_le_of_mul_le_leftₚ ← mul_le_of_mul_le_of_nonneg_left
+alias mul_lt_of_mul_lt_leftₚ ← mul_lt_of_mul_lt_of_nonneg_left
+alias le_mul_of_le_mul_leftₚ ← le_mul_of_le_mul_of_nonneg_left
+alias lt_mul_of_lt_mul_leftₚ ← lt_mul_of_lt_mul_of_nonneg_left
+alias mul_le_of_mul_le_rightₚ ← mul_le_of_mul_le_of_nonneg_right
+alias mul_lt_of_mul_lt_rightₚ ← mul_lt_of_mul_lt_of_nonneg_right
+alias le_mul_of_le_mul_rightₚ ← le_mul_of_le_mul_of_nonneg_right
+alias lt_mul_of_lt_mul_rightₚ ← lt_mul_of_lt_mul_of_nonneg_right
 
 end Preorder
 
@@ -352,34 +389,23 @@ theorem pos_iff_pos_of_mul_pos [PosMulReflectLT α] [MulPosReflectLT α] (hab :
     0 < a ↔ 0 < b :=
   ⟨pos_of_mul_pos_right hab ∘ le_of_lt, pos_of_mul_pos_left hab ∘ le_of_lt⟩
 
-theorem mul_le_mul_of_le_of_le [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a)
-    (d0 : 0 ≤ d) : a * c ≤ b * d :=
-  (mul_le_mul_of_nonneg_left h₂ a0).trans <| mul_le_mul_of_nonneg_right h₁ d0
+/-- Assumes left strict covariance. -/
+theorem left.mul_lt_mulₚ [PosMulStrictMono α] [MulPosMono α]
+    (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
+  mul_lt_mul_of_le_of_ltₚ' h₁.le h₂ c0 (a0.trans_lt h₁)
 
-theorem mul_le_mul [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c)
-    (b0 : 0 ≤ b) : a * c ≤ b * d :=
-  (mul_le_mul_of_nonneg_right h₁ c0).trans <| mul_le_mul_of_nonneg_left h₂ b0
+/-- Assumes right strict covariance. -/
+theorem right.mul_lt_mulₚ [PosMulMono α] [MulPosStrictMono α]
+    (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
+  mul_lt_mul_of_lt_of_leₚ h₁ h₂.le a0 (c0.trans_lt h₂)
+
+alias left.mul_lt_mulₚ ← mul_lt_mulₚ
+alias left.mul_lt_mulₚ ← mul_lt_mul'' -- this name was in `Algebra.Order.Ring.Defs`
 
 theorem mul_self_le_mul_self [PosMulMono α] [MulPosMono α] (ha : 0 ≤ a) (hab : a ≤ b) :
     a * a ≤ b * b :=
   mul_le_mul hab hab ha <| ha.trans hab
 
-theorem mul_le_of_mul_le_of_nonneg_left [PosMulMono α] (h : a * b ≤ c) (hle : d ≤ b)
-    (a0 : 0 ≤ a) : a * d ≤ c :=
-  (mul_le_mul_of_nonneg_left hle a0).trans h
-
-theorem le_mul_of_le_mul_of_nonneg_left [PosMulMono α] (h : a ≤ b * c) (hle : c ≤ d)
-    (b0 : 0 ≤ b) : a ≤ b * d :=
-  h.trans (mul_le_mul_of_nonneg_left hle b0)
-
-theorem mul_le_of_mul_le_of_nonneg_right [MulPosMono α] (h : a * b ≤ c) (hle : d ≤ a)
-    (b0 : 0 ≤ b) : d * b ≤ c :=
-  (mul_le_mul_of_nonneg_right hle b0).trans h
-
-theorem le_mul_of_le_mul_of_nonneg_right [MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d)
-    (c0 : 0 ≤ c) : a ≤ d * c :=
-  h.trans (mul_le_mul_of_nonneg_right hle c0)
-
 end Preorder
 
 section PartialOrder
@@ -476,7 +502,7 @@ theorem mul_eq_mul_iff_eq_and_eq_of_pos [PosMulStrictMono α] [MulPosStrictMono
   rcases eq_or_lt_of_le hbd with (rfl | hbd)
   · exact ⟨(mul_right_cancel_iff_of_pos d0).mp h, rfl⟩
 
-  exact ((mul_lt_mul_of_pos_of_pos hac hbd a0 d0).ne h).elim
+  exact ((mul_lt_mul_of_lt_of_ltₚ hac hbd a0 d0).ne h).elim
 
 theorem mul_eq_mul_iff_eq_and_eq_of_pos' [PosMulStrictMono α] [MulPosStrictMono α] [PosMulMonoRev α]
     [MulPosMonoRev α] (hac : a ≤ b) (hbd : c ≤ d) (b0 : 0 < b) (c0 : 0 < c) :
@@ -488,7 +514,7 @@ theorem mul_eq_mul_iff_eq_and_eq_of_pos' [PosMulStrictMono α] [MulPosStrictMono
   rcases eq_or_lt_of_le hbd with (rfl | hbd)
   · exact ⟨(mul_right_cancel_iff_of_pos c0).mp h, rfl⟩
 
-  exact ((mul_lt_mul_of_lt_of_lt' hac hbd b0 c0).ne h).elim
+  exact ((mul_lt_mul_of_lt_of_ltₚ' hac hbd c0 b0).ne h).elim
 
 end PartialOrder
 
@@ -516,17 +542,21 @@ theorem neg_of_mul_pos_left [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha
 theorem neg_iff_neg_of_mul_pos [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : a < 0 ↔ b < 0 :=
   ⟨neg_of_mul_pos_right hab ∘ le_of_lt, neg_of_mul_pos_left hab ∘ le_of_lt⟩
 
-theorem Left.neg_of_mul_neg_left [PosMulMono α] (h : a * b < 0) (h1 : 0 ≤ a) : b < 0 :=
-  lt_of_not_ge fun h2 : b ≥ 0 => (Left.mul_nonneg h1 h2).not_lt h
+theorem Left.neg_of_mul_neg_right [PosMulMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0 :=
+  lt_of_not_ge fun b0 : b ≥ 0 => (Left.mul_nonneg a0 b0).not_lt h
+
+alias Left.neg_of_mul_neg_right ← neg_of_mul_neg_right
+
+theorem Right.neg_of_mul_neg_right [MulPosMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0 :=
+  lt_of_not_ge fun b0 : b ≥ 0 => (Right.mul_nonneg a0 b0).not_lt h
 
-theorem Right.neg_of_mul_neg_left [MulPosMono α] (h : a * b < 0) (h1 : 0 ≤ a) : b < 0 :=
-  lt_of_not_ge fun h2 : b ≥ 0 => (Right.mul_nonneg h1 h2).not_lt h
+theorem Left.neg_of_mul_neg_left [PosMulMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0 :=
+  lt_of_not_ge fun a0 : a ≥ 0 => (Left.mul_nonneg a0 b0).not_lt h
 
-theorem Left.neg_of_mul_neg_right [PosMulMono α] (h : a * b < 0) (h1 : 0 ≤ b) : a < 0 :=
-  lt_of_not_ge fun h2 : a ≥ 0 => (Left.mul_nonneg h2 h1).not_lt h
+alias Left.neg_of_mul_neg_left ← neg_of_mul_neg_left
 
-theorem Right.neg_of_mul_neg_right [MulPosMono α] (h : a * b < 0) (h1 : 0 ≤ b) : a < 0 :=
-  lt_of_not_ge fun h2 : a ≥ 0 => (Right.mul_nonneg h2 h1).not_lt h
+theorem Right.neg_of_mul_neg_left [MulPosMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0 :=
+  lt_of_not_ge fun a0 : a ≥ 0 => (Right.mul_nonneg a0 b0).not_lt h
 
 end LinearOrder