chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -249,7 +249,7 @@ lemma short_needle_inter_eq (h : l ≤ d) (θ : ℝ) :
     Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2) := by
   rw [Set.Icc_inter_Icc, inf_eq_min, sup_eq_max, max_div_div_right zero_le_two,
     min_div_div_right zero_le_two, neg_mul, max_neg_neg, mul_comm,
-    min_eq_right (mul_le_of_le_of_le_one_of_nonneg h θ.sin_le_one hl.le)]
+    min_eq_right ((mul_le_of_le_one_right hl.le θ.sin_le_one).trans h)]
 
 include hd hBₘ hB hl in
 /--

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -703,6 +703,102 @@ theorem mul_lt_of_lt_one_right [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) :
 theorem lt_mul_of_one_lt_right [PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) : a < a * b := by
   simpa only [mul_one] using mul_lt_mul_of_pos_left h ha
 
+/-! Lemmas of the form `a ≤ 1 → b ≤ 1 → a * b ≤ 1`. -/
+
+/-- Assumes left covariance. -/
+theorem mul_le_one_left [PosMulMono α]
+    (ha : a ≤ 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b ≤ 1 :=
+  (mul_le_of_le_one_right a0 hb).trans ha
+
+/-- Assumes left covariance. -/
+theorem mul_lt_one_of_le_of_lt_left [PosMulStrictMono α]
+    (ha : a ≤ 1) (hb : b < 1) (a0 : 0 < a) : a * b < 1 :=
+  (mul_lt_of_lt_one_right a0 hb).trans_le ha
+
+/-- Assumes left covariance. -/
+theorem mul_lt_one_of_lt_of_le_left [PosMulMono α]
+    (ha : a < 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b < 1 :=
+  (mul_le_of_le_one_right a0 hb).trans_lt ha
+
+/-- Assumes left covariance. -/
+theorem mul_lt_one_left [PosMulStrictMono α]
+    (ha : a < 1) (hb : b < 1) (a0 : 0 < a) : a * b < 1 :=
+  (mul_lt_of_lt_one_right a0 hb).trans ha
+
+/-- Assumes right covariance. -/
+theorem mul_le_one_right [MulPosMono α]
+    (ha : a ≤ 1) (hb : b ≤ 1) (b0 : 0 ≤ b) : a * b ≤ 1 :=
+  (mul_le_of_le_one_left b0 ha).trans hb
+
+/-- Assumes right covariance. -/
+theorem mul_lt_one_of_lt_of_le_right [MulPosStrictMono α]
+    (ha : a < 1) (hb : b ≤ 1) (b0 : 0 < b) : a * b < 1 :=
+  (mul_lt_of_lt_one_left b0 ha).trans_le hb
+
+/-- Assumes right covariance. -/
+theorem mul_lt_one_of_le_of_lt_right [MulPosMono α]
+    (ha : a ≤ 1) (hb : b < 1) (b0 : 0 ≤ b) : a * b < 1 :=
+  (mul_le_of_le_one_left b0 ha).trans_lt hb
+
+/-- Assumes right covariance. -/
+theorem mul_lt_one_right [MulPosStrictMono α]
+    (ha : a < 1) (hb : b < 1) (b0 : 0 < b) : a * b < 1 :=
+  (mul_lt_of_lt_one_left b0 ha).trans hb
+
+theorem mul_lt_one_of_nonneg_of_lt_one_left [PosMulMono α]
+    (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : a * b < 1 :=
+  mul_lt_one_of_lt_of_le_left ha hb ha₀
+
+theorem mul_lt_one_of_nonneg_of_lt_one_right [MulPosMono α]
+    (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1 :=
+  mul_lt_one_of_le_of_lt_right ha hb hb₀
+
+/-! Lemmas of the form `1 ≤ a → 1 ≤ b → 1 ≤ a * b`. -/
+
+/-- Assumes left covariance. -/
+theorem Left.one_le_mul₀ [PosMulMono α] [ZeroLEOneClass α]
+    (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b :=
+  ha.trans (le_mul_of_one_le_right (zero_le_one.trans ha) hb)
+
+-- See `Left.one_lt_mul_of_le_of_lt₀` for `1 ≤ a → 1 < b → 1 < a * b`
+-- It's not here because we do not have `ZeroLTOneClass`. We need `PartialOrder` to show `0 < 1`.
+
+/-- Assumes left covariance. -/
+theorem Left.one_lt_mul_of_lt_of_le₀ [PosMulMono α] [ZeroLEOneClass α]
+    (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b :=
+  ha.trans_le (le_mul_of_one_le_right (zero_le_one.trans ha.le) hb)
+
+/-- Assumes left covariance. -/
+theorem Left.one_lt_mul₀ [PosMulStrictMono α] [ZeroLEOneClass α]
+    (ha : 1 < a) (hb : 1 < b) : 1 < a * b :=
+  ha.trans (lt_mul_of_one_lt_right (zero_le_one.trans_lt ha) hb)
+
+/-- Assumes right covariance. -/
+theorem Right.one_le_mul₀ [MulPosMono α] [ZeroLEOneClass α]
+    (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b :=
+  hb.trans (le_mul_of_one_le_left (zero_le_one.trans hb) ha)
+
+-- See `Right.one_lt_mul_of_lt_of_le₀` for `1 < a → 1 ≤ b → 1 < a * b`
+-- It's not here because we do not have `ZeroLTOneClass`. We need `PartialOrder` to show `0 < 1`.
+
+/-- Assumes right covariance. -/
+theorem Right.one_lt_mul_of_le_of_lt₀ [MulPosMono α] [ZeroLEOneClass α]
+    (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
+  hb.trans_le (le_mul_of_one_le_left (zero_le_one.trans hb.le) ha)
+
+/-- Assumes right covariance. -/
+theorem Right.one_lt_mul₀ [MulPosStrictMono α] [ZeroLEOneClass α]
+    (ha : 1 < a) (hb : 1 < b) : 1 < a * b :=
+  hb.trans (lt_mul_of_one_lt_left (zero_le_one.trans_lt hb) ha)
+
+alias one_le_mul_of_le_of_le := Left.one_le_mul₀
+alias one_lt_mul_of_le_of_lt := Right.one_lt_mul_of_le_of_lt₀
+alias one_lt_mul_of_lt_of_le := Left.one_lt_mul_of_lt_of_le₀
+alias one_lt_mul_of_lt_of_lt := Left.one_lt_mul₀
+
+alias one_le_mul_of_one_le_of_one_le := one_le_mul_of_le_of_le
+alias one_lt_mul := one_lt_mul_of_le_of_lt
+
 /-! Lemmas of the form `b ≤ c → a ≤ 1 → b * a ≤ c`. -/
 
 
@@ -722,16 +818,19 @@ theorem mul_lt_of_lt_of_le_one_of_nonneg [PosMulMono α] (h : b < c) (ha : a ≤
   (mul_le_of_le_one_right hb ha).trans_lt h
 
 /-- Assumes left covariance. -/
+@[deprecated mul_le_one_left (since := "2024-10-10")]
 theorem Left.mul_le_one_of_le_of_le [PosMulMono α] (ha : a ≤ 1) (hb : b ≤ 1) (a0 : 0 ≤ a) :
     a * b ≤ 1 :=
   mul_le_of_le_of_le_one_of_nonneg ha hb a0
 
 /-- Assumes left covariance. -/
+@[deprecated mul_lt_one_of_le_of_lt_left (since := "2024-10-10")]
 theorem Left.mul_lt_of_le_of_lt_one_of_pos [PosMulStrictMono α] (ha : a ≤ 1) (hb : b < 1)
     (a0 : 0 < a) : a * b < 1 :=
   _root_.mul_lt_of_le_of_lt_one_of_pos ha hb a0
 
 /-- Assumes left covariance. -/
+@[deprecated mul_lt_one_of_lt_of_le_left (since := "2024-10-10")]
 theorem Left.mul_lt_of_lt_of_le_one_of_nonneg [PosMulMono α] (ha : a < 1) (hb : b ≤ 1)
     (a0 : 0 ≤ a) : a * b < 1 :=
   _root_.mul_lt_of_lt_of_le_one_of_nonneg ha hb a0
@@ -767,162 +866,218 @@ theorem lt_mul_of_lt_of_one_le_of_nonneg [PosMulMono α] (h : b < c) (ha : 1 ≤
     b < c * a :=
   h.trans_le <| le_mul_of_one_le_right hc ha
 
+set_option linter.deprecated false
+
 /-- Assumes left covariance. -/
+@[deprecated Left.one_le_mul₀ (since := "2024-10-10")]
 theorem Left.one_le_mul_of_le_of_le [PosMulMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (a0 : 0 ≤ a) :
     1 ≤ a * b :=
   le_mul_of_le_of_one_le_of_nonneg ha hb a0
 
 /-- Assumes left covariance. -/
+@[deprecated (since := "2024-10-10")]
 theorem Left.one_lt_mul_of_le_of_lt_of_pos [PosMulStrictMono α] (ha : 1 ≤ a) (hb : 1 < b)
     (a0 : 0 < a) : 1 < a * b :=
   lt_mul_of_le_of_one_lt_of_pos ha hb a0
 
 /-- Assumes left covariance. -/
+@[deprecated Left.one_lt_mul_of_lt_of_le₀ (since := "2024-10-10")]
 theorem Left.lt_mul_of_lt_of_one_le_of_nonneg [PosMulMono α] (ha : 1 < a) (hb : 1 ≤ b)
     (a0 : 0 ≤ a) : 1 < a * b :=
   _root_.lt_mul_of_lt_of_one_le_of_nonneg ha hb a0
 
+@[deprecated (since := "2024-10-10")]
 theorem le_mul_of_le_of_one_le' [PosMulMono α] [MulPosMono α] (bc : b ≤ c) (ha : 1 ≤ a)
     (a0 : 0 ≤ a) (b0 : 0 ≤ b) : b ≤ c * a :=
   (le_mul_of_one_le_right b0 ha).trans <| mul_le_mul_of_nonneg_right bc a0
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_le_of_one_lt' [PosMulStrictMono α] [MulPosMono α] (bc : b ≤ c) (ha : 1 < a)
     (a0 : 0 ≤ a) (b0 : 0 < b) : b < c * a :=
   (lt_mul_of_one_lt_right b0 ha).trans_le <| mul_le_mul_of_nonneg_right bc a0
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_lt_of_one_le' [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : 1 ≤ a)
     (a0 : 0 < a) (b0 : 0 ≤ b) : b < c * a :=
   (le_mul_of_one_le_right b0 ha).trans_lt <| mul_lt_mul_of_pos_right bc a0
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_lt_of_one_lt_of_pos [PosMulStrictMono α] [MulPosStrictMono α] (bc : b < c)
     (ha : 1 < a) (a0 : 0 < a) (b0 : 0 < b) : b < c * a :=
   (lt_mul_of_one_lt_right b0 ha).trans <| mul_lt_mul_of_pos_right bc a0
 
 /-! Lemmas of the form `a ≤ 1 → b ≤ c → a * b ≤ c`. -/
 
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_le_of_le_one_of_le_of_nonneg [MulPosMono α] (ha : a ≤ 1) (h : b ≤ c) (hb : 0 ≤ b) :
     a * b ≤ c :=
   (mul_le_of_le_one_left hb ha).trans h
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_lt_of_lt_one_of_le_of_pos [MulPosStrictMono α] (ha : a < 1) (h : b ≤ c) (hb : 0 < b) :
     a * b < c :=
   (mul_lt_of_lt_one_left hb ha).trans_le h
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_lt_of_le_one_of_lt_of_nonneg [MulPosMono α] (ha : a ≤ 1) (h : b < c) (hb : 0 ≤ b) :
     a * b < c :=
   (mul_le_of_le_one_left hb ha).trans_lt h
 
 /-- Assumes right covariance. -/
+@[deprecated mul_lt_one_of_lt_of_le_right (since := "2024-10-10")]
 theorem Right.mul_lt_one_of_lt_of_le_of_pos [MulPosStrictMono α] (ha : a < 1) (hb : b ≤ 1)
     (b0 : 0 < b) : a * b < 1 :=
   mul_lt_of_lt_one_of_le_of_pos ha hb b0
 
 /-- Assumes right covariance. -/
+@[deprecated mul_lt_one_of_lt_of_le_right (since := "2024-10-10")]
 theorem Right.mul_lt_one_of_le_of_lt_of_nonneg [MulPosMono α] (ha : a ≤ 1) (hb : b < 1)
     (b0 : 0 ≤ b) : a * b < 1 :=
   mul_lt_of_le_one_of_lt_of_nonneg ha hb b0
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_lt_of_lt_one_of_lt_of_pos [PosMulStrictMono α] [MulPosStrictMono α] (ha : a < 1)
     (bc : b < c) (a0 : 0 < a) (c0 : 0 < c) : a * b < c :=
   (mul_lt_mul_of_pos_left bc a0).trans <| mul_lt_of_lt_one_left c0 ha
 
 /-- Assumes right covariance. -/
+@[deprecated mul_le_one_right (since := "2024-10-10")]
 theorem Right.mul_le_one_of_le_of_le [MulPosMono α] (ha : a ≤ 1) (hb : b ≤ 1) (b0 : 0 ≤ b) :
     a * b ≤ 1 :=
   mul_le_of_le_one_of_le_of_nonneg ha hb b0
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_le_of_le_one_of_le' [PosMulMono α] [MulPosMono α] (ha : a ≤ 1) (bc : b ≤ c) (a0 : 0 ≤ a)
     (c0 : 0 ≤ c) : a * b ≤ c :=
   (mul_le_mul_of_nonneg_left bc a0).trans <| mul_le_of_le_one_left c0 ha
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_lt_of_lt_one_of_le' [PosMulMono α] [MulPosStrictMono α] (ha : a < 1) (bc : b ≤ c)
     (a0 : 0 ≤ a) (c0 : 0 < c) : a * b < c :=
   (mul_le_mul_of_nonneg_left bc a0).trans_lt <| mul_lt_of_lt_one_left c0 ha
 
+@[deprecated (since := "2024-10-10")]
 theorem mul_lt_of_le_one_of_lt' [PosMulStrictMono α] [MulPosMono α] (ha : a ≤ 1) (bc : b < c)
     (a0 : 0 < a) (c0 : 0 ≤ c) : a * b < c :=
   (mul_lt_mul_of_pos_left bc a0).trans_le <| mul_le_of_le_one_left c0 ha
 
 /-! Lemmas of the form `1 ≤ a → b ≤ c → b ≤ a * c`. -/
 
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_one_lt_of_le_of_pos [MulPosStrictMono α] (ha : 1 < a) (h : b ≤ c) (hc : 0 < c) :
     b < a * c :=
   h.trans_lt <| lt_mul_of_one_lt_left hc ha
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_one_le_of_lt_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) :
     b < a * c :=
   h.trans_le <| le_mul_of_one_le_left hc ha
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_one_lt_of_lt_of_pos [MulPosStrictMono α] (ha : 1 < a) (h : b < c) (hc : 0 < c) :
     b < a * c :=
   h.trans <| lt_mul_of_one_lt_left hc ha
 
 /-- Assumes right covariance. -/
+@[deprecated (since := "2024-10-10")]
 theorem Right.one_lt_mul_of_lt_of_le_of_pos [MulPosStrictMono α] (ha : 1 < a) (hb : 1 ≤ b)
     (b0 : 0 < b) : 1 < a * b :=
   lt_mul_of_one_lt_of_le_of_pos ha hb b0
 
 /-- Assumes right covariance. -/
+@[deprecated Right.one_lt_mul_of_le_of_lt₀ (since := "2024-10-10")]
 theorem Right.one_lt_mul_of_le_of_lt_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (hb : 1 < b)
     (b0 : 0 ≤ b) : 1 < a * b :=
   lt_mul_of_one_le_of_lt_of_nonneg ha hb b0
 
 /-- Assumes right covariance. -/
+@[deprecated Right.one_lt_mul₀ (since := "2024-10-10")]
 theorem Right.one_lt_mul_of_lt_of_lt [MulPosStrictMono α] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) :
     1 < a * b :=
   lt_mul_of_one_lt_of_lt_of_pos ha hb b0
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_mul_of_one_lt_of_lt_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) :
     b < a * c :=
   h.trans_le <| le_mul_of_one_le_left hc ha
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_of_mul_lt_of_one_le_of_nonneg_left [PosMulMono α] (h : a * b < c) (hle : 1 ≤ b)
     (ha : 0 ≤ a) : a < c :=
   (le_mul_of_one_le_right ha hle).trans_lt h
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_of_lt_mul_of_le_one_of_nonneg_left [PosMulMono α] (h : a < b * c) (hc : c ≤ 1)
     (hb : 0 ≤ b) : a < b :=
   h.trans_le <| mul_le_of_le_one_right hb hc
 
+@[deprecated (since := "2024-10-10")]
 theorem lt_of_lt_mul_of_le_one_of_nonneg_right [MulPosMono α] (h : a < b * c) (hb : b ≤ 1)
     (hc : 0 ≤ c) : a < c :=
   h.trans_le <| mul_le_of_le_one_left hc hb
 
+@[deprecated (since := "2024-10-10")]
 theorem le_mul_of_one_le_of_le_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (bc : b ≤ c) (c0 : 0 ≤ c) :
     b ≤ a * c :=
   bc.trans <| le_mul_of_one_le_left c0 ha
 
 /-- Assumes right covariance. -/
+@[deprecated Right.one_le_mul₀ (since := "2024-10-10")]
 theorem Right.one_le_mul_of_le_of_le [MulPosMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (b0 : 0 ≤ b) :
     1 ≤ a * b :=
   le_mul_of_one_le_of_le_of_nonneg ha hb b0
 
+@[deprecated (since := "2024-10-10")]
 theorem le_of_mul_le_of_one_le_of_nonneg_left [PosMulMono α] (h : a * b ≤ c) (hb : 1 ≤ b)
     (ha : 0 ≤ a) : a ≤ c :=
   (le_mul_of_one_le_right ha hb).trans h
 
+@[deprecated (since := "2024-10-10")]
 theorem le_of_le_mul_of_le_one_of_nonneg_left [PosMulMono α] (h : a ≤ b * c) (hc : c ≤ 1)
     (hb : 0 ≤ b) : a ≤ b :=
   h.trans <| mul_le_of_le_one_right hb hc
 
+@[deprecated (since := "2024-10-10")]
 theorem le_of_mul_le_of_one_le_nonneg_right [MulPosMono α] (h : a * b ≤ c) (ha : 1 ≤ a)
     (hb : 0 ≤ b) : b ≤ c :=
   (le_mul_of_one_le_left hb ha).trans h
 
+@[deprecated (since := "2024-10-10")]
 theorem le_of_le_mul_of_le_one_of_nonneg_right [MulPosMono α] (h : a ≤ b * c) (hb : b ≤ 1)
     (hc : 0 ≤ c) : a ≤ c :=
   h.trans <| mul_le_of_le_one_left hc hb
 
 end Preorder
 
+section PartialOrder
+
+variable [PartialOrder α]
+
+/-- Assumes left covariance. -/
+theorem Left.one_lt_mul_of_le_of_lt₀ [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero (1 : α)]
+    (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
+  ha.trans_lt (lt_mul_of_one_lt_right (zero_lt_one.trans_le ha) hb)
+
+attribute [deprecated Left.one_lt_mul_of_le_of_lt₀ (since := "2024-10-10")]
+  Left.one_lt_mul_of_le_of_lt_of_pos
+
+/-- Assumes right covariance. -/
+theorem Right.one_lt_mul_of_lt_of_le₀ [MulPosStrictMono α] [ZeroLEOneClass α] [NeZero (1 : α)]
+    (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b :=
+  hb.trans_lt (lt_mul_of_one_lt_left (zero_lt_one.trans_le hb) ha)
+
+attribute [deprecated Right.one_lt_mul_of_lt_of_le₀ (since := "2024-10-10")]
+  Right.one_lt_mul_of_lt_of_le_of_pos
+
+end PartialOrder
+
 section LinearOrder
 
 variable [LinearOrder α]
 
--- Yaël: What's the point of this lemma? If we have `0 * 0 = 0`, then we can just take `b = 0`.
--- proven with `a0 : 0 ≤ a` as `exists_square_le`
+@[deprecated (since := "2024-10-10")]
 theorem exists_square_le' [PosMulStrictMono α] (a0 : 0 < a) : ∃ b : α, b * b ≤ a := by
   obtain ha | ha := lt_or_le a 1
   · exact ⟨a, (mul_lt_of_lt_one_right a0 ha).le⟩
@@ -960,23 +1115,6 @@ lemma pow_le_of_le_one [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀]
 lemma sq_le [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) :
     a ^ 2 ≤ a := pow_le_of_le_one h₀ h₁ two_ne_zero
 
-lemma one_le_mul_of_one_le_of_one_le [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hb : 1 ≤ b) :
-    (1 : M₀) ≤ a * b := Left.one_le_mul_of_le_of_le ha hb <| zero_le_one.trans ha
-
-lemma one_lt_mul_of_le_of_lt [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) :
-    1 < a * b := hb.trans_le <| le_mul_of_one_le_left (zero_le_one.trans hb.le) ha
-
-lemma one_lt_mul_of_lt_of_le [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 ≤ b) :
-    1 < a * b := ha.trans_le <| le_mul_of_one_le_right (zero_le_one.trans ha.le) hb
-
-alias one_lt_mul := one_lt_mul_of_le_of_lt
-
-lemma mul_lt_one_of_nonneg_of_lt_one_left [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) :
-    a * b < 1 := (mul_le_of_le_one_right ha₀ hb).trans_lt ha
-
-lemma mul_lt_one_of_nonneg_of_lt_one_right [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) :
-    a * b < 1 := (mul_le_of_le_one_left hb₀ ha).trans_lt hb
-
 section
 variable [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀]
 

Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

@@ -50,7 +50,7 @@ private lemma edgeDensity_badVertices_le (hε : 0 ≤ ε) (dst : 2 * ε ≤ G.ed
 
 private lemma card_badVertices_le (dst : 2 * ε ≤ G.edgeDensity s t) (hst : G.IsUniform ε s t) :
     (badVertices G ε s t).card ≤ s.card * ε := by
-  have hε : ε ≤ 1 := (le_mul_of_one_le_of_le_of_nonneg (by norm_num) le_rfl hst.pos.le).trans
+  have hε : ε ≤ 1 := (le_mul_of_one_le_left hst.pos.le (by norm_num)).trans
     (dst.trans <| by exact_mod_cast edgeDensity_le_one _ _ _)
   by_contra! h
   have : |(G.edgeDensity (badVertices G ε s t) t - G.edgeDensity s t : ℝ)| < ε :=

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

@@ -287,7 +287,7 @@ theorem algebraMap' (k : K) : (_root_.algebraMap K (K_hat R K) k).IsFiniteAdele
     contrapose! this
     change 1 < v.intValuation n
     rw [← hk, mul_comm]
-    exact lt_mul_of_le_of_one_lt' this hv (by simp) (by simp)
+    exact one_lt_mul_of_le_of_lt this hv
   simp_rw [valuation_of_algebraMap]
   change {v : HeightOneSpectrum R | v.intValuationDef d < 1}.Finite
   simp_rw [intValuation_lt_one_iff_dvd]