chore: generalise more lemmas from LinearOrderedField to `GroupWith…

…Zero` (#17359)

... and move the lemmas from `Algebra.Order.Field.Basic` to `Algebra.Order.GroupWithZero.Unbundled`. Also take the opportunity to add `₀` at the end, per the naming convention.

Archive/Imo/Imo1972Q5.lean

@@ -50,7 +50,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
       calc
         0 < ‖f x‖ := norm_pos_iff.mpr hx
         _ ≤ k := hk₁ x
-    rw [div_lt_iff]
+    rw [div_lt_iff₀]
     · apply lt_mul_of_one_lt_right h₁ hneg
     · exact zero_lt_one.trans hneg
   -- Demonstrate that `k ≤ k'` using `hk₂`.
@@ -87,7 +87,7 @@ theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x -
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2
   have hgy : 0 < ‖g y‖ := by linarith
   have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x)
-  have : k / ‖g y‖ < k := (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right k_pos H)
+  have : k / ‖g y‖ < k := (div_lt_iff₀ hgy).mpr (lt_mul_of_one_lt_right k_pos H)
   have : k ≤ k / ‖g y‖ := by
     suffices ∀ x, ‖f x‖ ≤ k / ‖g y‖ from ciSup_le this
     intro x

Archive/Imo/Imo1986Q5.lean

@@ -54,7 +54,7 @@ theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
   have hx' : 0 < 2 - x := tsub_pos_of_lt hx
   have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
   apply le_antisymm
-  · rw [le_div_iff₀ hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
+  · rw [le_div_iff₀ hx', ← le_div_iff₀' hfx.bot_lt, tsub_le_iff_right, ← hf.map_eq_zero,
      hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
   · rw [div_le_iff₀' hx', ← hf.map_eq_zero]
     refine (mul_eq_zero.1 ?_).resolve_right hfx

Mathlib.lean

@@ -610,6 +610,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Canonical
 import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas
 import Mathlib.Algebra.Order.GroupWithZero.WithZero
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Hom.Monoid

Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -97,9 +97,9 @@ theorem of_convergence_epsilon :
     have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos
     have nB_pos : 0 < nB := nB_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
     have zero_lt_mul_conts : 0 < B * nB := by positivity
-    suffices 1 < ε * (B * nB) from (div_lt_iff zero_lt_mul_conts).mpr this
+    suffices 1 < ε * (B * nB) from (div_lt_iff₀ zero_lt_mul_conts).mpr this
     -- use that `N' ≥ n` was obtained from the archimedean property to show the following
-    calc 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
+    calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
       _ ≤ ε * (B * nB) := ?_
     -- cancel `ε`
     gcongr

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -223,7 +223,7 @@ variable [LinearOrderedSemifield α] [Archimedean α] {x y ε : α}
 lemma exists_nat_one_div_lt (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1 : α) < ε := by
   cases' exists_nat_gt (1 / ε) with n hn
   use n
-  rw [div_lt_iff, ← div_lt_iff' hε]
+  rw [div_lt_iff₀, ← div_lt_iff₀' hε]
   · apply hn.trans
     simp [zero_lt_one]
   · exact n.cast_add_one_pos
@@ -299,11 +299,11 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
   refine ⟨(z + 1 : ℤ) / n, ?_⟩
   have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
   have n0 := Nat.cast_pos.1 n0'
-  rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff n0']
-  · refine ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩
+  rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff₀ n0']
+  · refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩
     rw [Int.cast_add, Int.cast_one]
     refine lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) ?_
-    rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
+    rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]
   · rw [Rat.den_intCast, Nat.cast_one]
     exact one_ne_zero
   · intro H
@@ -352,7 +352,7 @@ variable [LinearOrderedField α]
 theorem archimedean_iff_nat_lt : Archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
   ⟨@exists_nat_gt α _, fun H =>
     ⟨fun x y y0 =>
-      (H (x / y)).imp fun n h => le_of_lt <| by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
+      (H (x / y)).imp fun n h => le_of_lt <| by rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h⟩⟩
 
 theorem archimedean_iff_nat_le : Archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
   archimedean_iff_nat_lt.trans

Mathlib/Algebra/Order/Field/Basic.lean

@@ -5,6 +5,7 @@ Authors: Robert Y. Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.Order.Field.Defs
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Tactic.Bound.Attribute
@@ -23,55 +24,46 @@ section LinearOrderedSemifield
 
 variable [LinearOrderedSemifield α] {a b c d e : α} {m n : ℤ}
 
-/-- `Equiv.mulLeft₀` as an order_iso. -/
-@[simps! (config := { simpRhs := true })]
-def OrderIso.mulLeft₀ (a : α) (ha : 0 < a) : α ≃o α :=
-  { Equiv.mulLeft₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_left ha }
-
-/-- `Equiv.mulRight₀` as an order_iso. -/
-@[simps! (config := { simpRhs := true })]
-def OrderIso.mulRight₀ (a : α) (ha : 0 < a) : α ≃o α :=
-  { Equiv.mulRight₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_right ha }
-
 /-!
 ### Relating one division with another term.
 -/
 
-theorem lt_div_iff (hc : 0 < c) : a < b / c ↔ a * c < b :=
-  lt_iff_lt_of_le_iff_le <| div_le_iff₀ hc
-
-theorem lt_div_iff' (hc : 0 < c) : a < b / c ↔ c * a < b := by rw [mul_comm, lt_div_iff hc]
-
-theorem div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c :=
-  lt_iff_lt_of_le_iff_le (le_div_iff₀ hc)
+@[deprecated lt_div_iff₀ (since := "2024-10-02")]
+theorem lt_div_iff (hc : 0 < c) : a < b / c ↔ a * c < b := lt_div_iff₀ hc
 
-theorem div_lt_iff' (hc : 0 < c) : b / c < a ↔ b < c * a := by rw [mul_comm, div_lt_iff hc]
+@[deprecated lt_div_iff₀' (since := "2024-10-02")]
+theorem lt_div_iff' (hc : 0 < c) : a < b / c ↔ c * a < b := lt_div_iff₀' hc
 
-lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by
-  rw [div_lt_iff hb, div_lt_iff' hc]
+@[deprecated div_lt_iff₀ (since := "2024-10-02")]
+theorem div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c := div_lt_iff₀ hc
 
-theorem inv_mul_le_iff (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ b * c := by
-  rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div]
-  exact div_le_iff₀' h
+@[deprecated div_lt_iff₀' (since := "2024-10-02")]
+theorem div_lt_iff' (hc : 0 < c) : b / c < a ↔ b < c * a := div_lt_iff₀' hc
 
-theorem inv_mul_le_iff' (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ c * b := by rw [inv_mul_le_iff h, mul_comm]
+@[deprecated inv_mul_le_iff₀ (since := "2024-10-02")]
+theorem inv_mul_le_iff (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ b * c := inv_mul_le_iff₀ h
 
-theorem mul_inv_le_iff (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ b * c := by rw [mul_comm, inv_mul_le_iff h]
+set_option linter.docPrime false in
+@[deprecated inv_mul_le_iff₀' (since := "2024-10-02")]
+theorem inv_mul_le_iff' (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ c * b := inv_mul_le_iff₀' h
 
-theorem mul_inv_le_iff' (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := by rw [mul_comm, inv_mul_le_iff' h]
+@[deprecated mul_inv_le_iff₀' (since := "2024-10-02")]
+theorem mul_inv_le_iff (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ b * c := mul_inv_le_iff₀' h
 
-theorem div_self_le_one (a : α) : a / a ≤ 1 :=
-  if h : a = 0 then by simp [h] else by simp [h]
+@[deprecated mul_inv_le_iff₀ (since := "2024-10-02")]
+theorem mul_inv_le_iff' (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := mul_inv_le_iff₀ h
 
-theorem inv_mul_lt_iff (h : 0 < b) : b⁻¹ * a < c ↔ a < b * c := by
-  rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div]
-  exact div_lt_iff' h
+@[deprecated inv_mul_lt_iff₀ (since := "2024-10-02")]
+theorem inv_mul_lt_iff (h : 0 < b) : b⁻¹ * a < c ↔ a < b * c := inv_mul_lt_iff₀ h
 
-theorem inv_mul_lt_iff' (h : 0 < b) : b⁻¹ * a < c ↔ a < c * b := by rw [inv_mul_lt_iff h, mul_comm]
+@[deprecated inv_mul_lt_iff₀' (since := "2024-10-02")]
+theorem inv_mul_lt_iff' (h : 0 < b) : b⁻¹ * a < c ↔ a < c * b := inv_mul_lt_iff₀' h
 
-theorem mul_inv_lt_iff (h : 0 < b) : a * b⁻¹ < c ↔ a < b * c := by rw [mul_comm, inv_mul_lt_iff h]
+@[deprecated mul_inv_lt_iff₀' (since := "2024-10-02")]
+theorem mul_inv_lt_iff (h : 0 < b) : a * b⁻¹ < c ↔ a < b * c := mul_inv_lt_iff₀' h
 
-theorem mul_inv_lt_iff' (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := by rw [mul_comm, inv_mul_lt_iff' h]
+@[deprecated mul_inv_lt_iff₀ (since := "2024-10-02")]
+theorem mul_inv_lt_iff' (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := mul_inv_lt_iff₀ h
 
 theorem inv_pos_le_iff_one_le_mul (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ b * a := by
   rw [inv_eq_one_div]
@@ -83,11 +75,11 @@ theorem inv_pos_le_iff_one_le_mul' (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ a * b :
 
 theorem inv_pos_lt_iff_one_lt_mul (ha : 0 < a) : a⁻¹ < b ↔ 1 < b * a := by
   rw [inv_eq_one_div]
-  exact div_lt_iff ha
+  exact div_lt_iff₀ ha
 
 theorem inv_pos_lt_iff_one_lt_mul' (ha : 0 < a) : a⁻¹ < b ↔ 1 < a * b := by
   rw [inv_eq_one_div]
-  exact div_lt_iff' ha
+  exact div_lt_iff₀' ha
 
 /-- One direction of `div_le_iff` where `b` is allowed to be `0` (but `c` must be nonnegative) -/
 theorem div_le_of_nonneg_of_le_mul (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c := by
@@ -237,7 +229,7 @@ theorem div_le_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c
   le_iff_le_iff_lt_iff_lt.2 (div_lt_div_left ha hc hb)
 
 theorem div_lt_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b < c / d ↔ a * d < c * b := by
-  rw [lt_div_iff d0, div_mul_eq_mul_div, div_lt_iff b0]
+  rw [lt_div_iff₀ d0, div_mul_eq_mul_div, div_lt_iff₀ b0]
 
 theorem div_le_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b := by
   rw [le_div_iff₀ d0, div_mul_eq_mul_div, div_le_iff₀ b0]
@@ -275,9 +267,9 @@ theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff
 
 theorem div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b := by rw [div_le_iff₀ hb, one_mul]
 
-theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a := by rw [lt_div_iff hb, one_mul]
+theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a := by rw [lt_div_iff₀ hb, one_mul]
 
-theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b := by rw [div_lt_iff hb, one_mul]
+theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b := by rw [div_lt_iff₀ hb, one_mul]
 
 theorem one_div_le (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a := by simpa using inv_le ha hb
 
@@ -300,7 +292,7 @@ theorem one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a :=
   simpa using inv_le_inv_of_le ha h
 
 theorem one_div_lt_one_div_of_lt (ha : 0 < a) (h : a < b) : 1 / b < 1 / a := by
-  rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
+  rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
 
 theorem le_of_one_div_le_one_div (ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a :=
   le_imp_le_of_lt_imp_lt (one_div_lt_one_div_of_lt ha) h
@@ -341,7 +333,7 @@ theorem half_le_self_iff : a / 2 ≤ a ↔ 0 ≤ a := by
 
 @[simp]
 theorem half_lt_self_iff : a / 2 < a ↔ 0 < a := by
-  rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
+  rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
 
 alias ⟨_, half_le_self⟩ := half_le_self_iff
 
@@ -355,9 +347,9 @@ theorem one_half_lt_one : (1 / 2 : α) < 1 :=
 theorem two_inv_lt_one : (2⁻¹ : α) < 1 :=
   (one_div _).symm.trans_lt one_half_lt_one
 
-theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff, mul_two]
+theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff₀, mul_two]
 
-theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff, mul_two]
+theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff₀, mul_two]
 
 theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by
   rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
@@ -385,12 +377,12 @@ theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) :
 theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a := by
   have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
   refine ⟨a / max (b + 1) 1, this, ?_⟩
-  rw [← lt_div_iff this, div_div_cancel' h.ne']
+  rw [← lt_div_iff₀ this, div_div_cancel' h.ne']
   exact lt_max_iff.2 (Or.inl <| lt_add_one _)
 
 theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
   let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b;
-  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩
+  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]⟩
 
 lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) :=
   fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha

Mathlib/Algebra/Order/Field/Pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Yaël Dillies
 -/
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
-import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.SMulWithZero
 
 /-!
@@ -33,7 +33,7 @@ theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
     · exact (mul_lt_mul_left hr).mpr a_h_left_right
   · rintro ⟨a_left, a_right⟩
     use x / r
-    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    refine ⟨⟨(lt_div_iff₀' hr).mpr a_left, (div_lt_iff₀' hr).mpr a_right⟩, ?_⟩
     rw [mul_div_cancel₀ _ (ne_of_gt hr)]
 
 theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
@@ -59,7 +59,7 @@ theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
     · exact (mul_lt_mul_left hr).mpr a_h_left_right
   · rintro ⟨a_left, a_right⟩
     use x / r
-    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff₀' hr).mpr a_right⟩, ?_⟩
     rw [mul_div_cancel₀ _ (ne_of_gt hr)]
 
 theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
@@ -72,7 +72,7 @@ theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
     · exact (mul_le_mul_left hr).mpr a_h_left_right
   · rintro ⟨a_left, a_right⟩
     use x / r
-    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
+    refine ⟨⟨(lt_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
     rw [mul_div_cancel₀ _ (ne_of_gt hr)]
 
 theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
@@ -84,7 +84,7 @@ theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
   · rintro h
     use x / r
     constructor
-    · exact (lt_div_iff' hr).mpr h
+    · exact (lt_div_iff₀' hr).mpr h
     · exact mul_div_cancel₀ _ (ne_of_gt hr)
 
 theorem smul_Iio : r • Iio a = Iio (r • a) := by
@@ -96,7 +96,7 @@ theorem smul_Iio : r • Iio a = Iio (r • a) := by
   · rintro h
     use x / r
     constructor
-    · exact (div_lt_iff' hr).mpr h
+    · exact (div_lt_iff₀' hr).mpr h
     · exact mul_div_cancel₀ _ (ne_of_gt hr)
 
 theorem smul_Ici : r • Ici a = Ici (r • a) := by

Mathlib/Algebra/Order/Floor.lean

@@ -484,7 +484,7 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   · exact div_nonneg ha n.cast_nonneg
   constructor
   · exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg)
-  rw [div_lt_iff, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]
+  rw [div_lt_iff₀, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]
   · exact lt_div_mul_add hn
   · exact cast_pos.2 hn
 
@@ -515,7 +515,7 @@ lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉
   obtain hab | hba := le_total a (b - 1)⁻¹
   · calc
       ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : α) := by gcongr
-      _ < b * a := by rwa [← div_lt_iff']; positivity
+      _ < b * a := by rwa [← div_lt_iff₀']; positivity
   · rw [← sub_pos] at hb
     calc
       ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
@@ -1027,7 +1027,7 @@ theorem sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ *
 theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
   sub_lt_iff_lt_add.2 <| by
     -- Porting note: `← one_add_mul` worked in mathlib3 without the argument
-    rw [← one_add_mul _ b, ← div_lt_iff hb, add_comm]
+    rw [← one_add_mul _ b, ← div_lt_iff₀ hb, add_comm]
     exact lt_floor_add_one _
 
 theorem fract_div_natCast_eq_div_natCast_mod {m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n := by
@@ -1261,15 +1261,15 @@ lemma ceil_div_ceil_inv_sub_one (ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ =
   have : 0 < ⌈(a - 1)⁻¹⌉ := ceil_pos.2 <| by positivity
   refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
   rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
-      ← lt_div_iff (sub_pos.2 <| inv_lt_one ha)]
+      ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one ha)]
   convert ceil_lt_add_one _ using 1
   field_simp
 
 lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉ / b < a) : ⌈a⌉ < b * a := by
   obtain hab | hba := le_total a (b - 1)⁻¹
   · calc
       ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
-      _ < b * a := by rwa [← div_lt_iff']; positivity
+      _ < b * a := by rwa [← div_lt_iff₀']; positivity
   · rw [← sub_pos] at hb
     calc
       ⌈a⌉ < a + 1 := ceil_lt_add_one _
@@ -1453,7 +1453,7 @@ section LinearOrderedField
 variable [LinearOrderedField α] [FloorRing α]
 
 theorem round_eq (x : α) : round x = ⌊x + 1 / 2⌋ := by
-  simp_rw [round, (by simp only [lt_div_iff', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)]
+  simp_rw [round, (by simp only [lt_div_iff₀', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)]
   cases' lt_or_le (fract x) (1 / 2) with hx hx
   · conv_rhs => rw [← fract_add_floor x, add_assoc, add_left_comm, floor_int_add]
     rw [if_pos hx, self_eq_add_right, floor_eq_iff, cast_zero, zero_add]

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -185,12 +185,6 @@ theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c := by
 theorem mul_lt_right₀ (c : α) (h : a < b) (hc : c ≠ 0) : a * c < b * c :=
   mul_lt_mul_of_pos_right h (zero_lt_iff.2 hc)
 
-theorem inv_lt_one₀ (ha : a ≠ 0) : a⁻¹ < 1 ↔ 1 < a :=
-  inv_lt_one' (a := Units.mk0 a ha)
-
-theorem one_lt_inv₀ (ha : a ≠ 0) : 1 < a⁻¹ ↔ a < 1 :=
-  one_lt_inv' (a := Units.mk0 a ha)
-
 theorem inv_lt_inv₀ (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a :=
   show (Units.mk0 a ha)⁻¹ < (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb < Units.mk0 a ha from
     have : CovariantClass αˣ αˣ (· * ·) (· < ·) :=