From 8d9d23b5bbb083ffd57d5bb700677dac1302cd32 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 2 Sep 2025 13:43:53 +1000
Subject: [PATCH] feat: (approximate) inverses of dyadic rationals (#10194)

This PR adds the inverse of a dyadic rational, at a given precision, and
characterising lemmas. Also cleans up various parts of the `Int.DivMod`
and `Rat` APIs, and proves some characterising lemmas about
`Rat.toDyadic`.

---------

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
---
 src/Init/Data/Dyadic.lean               |   1 +
 src/Init/Data/Dyadic/Basic.lean         | 108 +++++++++++++++++--
 src/Init/Data/Dyadic/Inv.lean           |  80 ++++++++++++++
 src/Init/Data/Int/DivMod/Bootstrap.lean |  48 ++++++---
 src/Init/Data/Int/DivMod/Lemmas.lean    | 102 ++++++++++++------
 src/Init/Data/Int/Lemmas.lean           |   2 +-
 src/Init/Data/Int/Linear.lean           |  10 +-
 src/Init/Data/Int/Order.lean            |   5 +-
 src/Init/Data/Rat/Basic.lean            |   3 +
 src/Init/Data/Rat/Lemmas.lean           | 135 +++++++++++++++++++++++-
 src/Init/Grind/Ring/Poly.lean           |   2 +-
 src/Init/Omega/Int.lean                 |   2 +-
 12 files changed, 428 insertions(+), 70 deletions(-)
 create mode 100644 src/Init/Data/Dyadic/Inv.lean

diff --git a/src/Init/Data/Dyadic.lean b/src/Init/Data/Dyadic.lean
index 7bc7bc55ff..49e3b55667 100644
--- a/src/Init/Data/Dyadic.lean
+++ b/src/Init/Data/Dyadic.lean
@@ -9,3 +9,4 @@ prelude
 public import Init.Data.Dyadic.Basic
 public import Init.Data.Dyadic.Instances
 public import Init.Data.Dyadic.Round
+public import Init.Data.Dyadic.Inv
diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean
index e9b0e4c373..3cd06e327d 100644
--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -75,7 +75,7 @@ theorem trailingZeros_two_mul {i : Int} (h : i ≠ 0) :
 
 theorem shiftRight_trailingZeros_mod_two {i : Int} (h : i ≠ 0) :
     (i >>> i.trailingZeros) % 2 = 1 := by
-  rw (occs := .pos [2]) [← Int.emod_add_ediv i 2]
+  rw (occs := .pos [2]) [← Int.emod_add_mul_ediv i 2]
   rcases i.emod_two_eq with h' | h' <;> rw [h']
   · rcases Int.dvd_of_emod_eq_zero h' with ⟨a, rfl⟩
     simp only [ne_eq, Int.mul_eq_zero, Int.reduceEq, false_or] at h
@@ -92,7 +92,7 @@ theorem two_pow_trailingZeros_dvd {i : Int} (h : i ≠ 0) :
     simp only [ne_eq, Int.mul_eq_zero, Int.reduceEq, false_or] at h
     rw [trailingZeros_two_mul h, Int.pow_succ']
     exact Int.mul_dvd_mul_left _ (two_pow_trailingZeros_dvd h)
-  · rw (occs := .pos [1]) [← Int.emod_add_ediv i 2, h', Int.add_comm, trailingZeros_two_mul_add_one]
+  · rw (occs := .pos [1]) [← Int.emod_add_mul_ediv i 2, h', Int.add_comm, trailingZeros_two_mul_add_one]
     exact Int.one_dvd _
 termination_by i.natAbs
 
@@ -415,16 +415,22 @@ theorem precision_ofIntWithPrec_le {i : Int} (h : i ≠ 0) (prec : Int) :
   | .zero => rfl
   | .ofOdd _ _ _ => rfl
 
+end Dyadic
+
+namespace Rat
+
+open Dyadic
+
 /--
 Convert a rational number `x` to the greatest dyadic number with precision at most `prec`
 which is less than or equal to `x`.
 -/
-def _root_.Rat.toDyadic (x : Rat) (prec : Int) : Dyadic :=
+def toDyadic (x : Rat) (prec : Int) : Dyadic :=
   match prec with
   | (n : Nat) => .ofIntWithPrec ((x.num <<< n) / x.den) prec
   | -(n + 1 : Nat) => .ofIntWithPrec (x.num / (x.den <<< (n + 1))) prec
 
-theorem _root_.Rat.toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
+theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
     Rat.toDyadic (mkRat a b) prec =
       .ofIntWithPrec ((a <<< prec.toNat) / (b <<< (-prec).toNat)) prec := by
   by_cases hb : b = 0
@@ -432,15 +438,96 @@ theorem _root_.Rat.toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
   rcases h : mkRat a b with ⟨n, d, hnz, hr⟩
   obtain ⟨m, hm, rfl, rfl⟩ := Rat.mkRat_num_den hb h
   cases prec
-  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_nat,
+  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast,
       shiftLeft_zero, Int.natCast_mul]
     rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
       Int.mul_ediv_cancel _ (by simpa using hm)]
   · simp only [Rat.toDyadic, Int.natCast_shiftLeft, Int.negSucc_eq, ← Int.natCast_add_one,
-      Int.toNat_neg_nat, Int.shiftLeft_zero, Int.neg_neg, Int.toNat_natCast, Int.natCast_mul]
+      Int.toNat_neg_natCast, Int.shiftLeft_zero, Int.neg_neg, Int.toNat_natCast, Int.natCast_mul]
     rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv (by simp),
       Int.mul_ediv_cancel _ (by simpa using hm)]
 
+theorem toDyadic_eq_ofIntWithPrec (x : Rat) (prec : Int) :
+    x.toDyadic prec = .ofIntWithPrec ((x.num <<< prec.toNat) / (x.den <<< (-prec).toNat)) prec := by
+  conv => lhs; rw [← Rat.mkRat_self x]
+  rw [Rat.toDyadic_mkRat]
+
+/--
+Converting a rational to a dyadic at a given precision and then back to a rational
+gives the same result as taking the floor of the rational at precision `2 ^ prec`.
+-/
+theorem toRat_toDyadic (x : Rat) (prec : Int) :
+    (x.toDyadic prec).toRat = (x * 2 ^ prec).floor / 2 ^ prec := by
+  rw [Rat.toDyadic_eq_ofIntWithPrec, toRat_ofIntWithPrec_eq_mul_two_pow, Rat.zpow_neg, Rat.div_def]
+  congr 2
+  rw [Rat.floor_def, Int.shiftLeft_eq, Nat.shiftLeft_eq]
+  match prec with
+  | .ofNat prec =>
+    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
+      Nat.mul_one]
+    have : (2 ^ prec : Rat) = ((2 ^ prec : Nat) : Rat) := by simp
+    rw [Rat.zpow_natCast, this, Rat.mul_def']
+    simp only [Rat.num_mkRat, Rat.den_mkRat]
+    simp only [Rat.natCast_pow, Rat.natCast_ofNat, Rat.num_pow, Rat.num_ofNat, Rat.den_pow,
+      Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
+    split
+    · simp_all
+    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+      congr 1
+      rw [Int.natCast_ediv, Int.mul_ediv_cancel']
+      rw [Int.natCast_dvd_natCast]
+      apply gcd_dvd_left
+  | .negSucc prec =>
+    simp only [Int.toNat_negSucc, Int.pow_zero, Int.mul_one, Int.neg_negSucc, Int.natCast_mul,
+      Int.natCast_pow, Int.cast_ofNat_Int]
+    have : (2 ^ ((prec : Int) + 1)) = ((2 ^ (prec + 1) : Nat) : Rat) := by simp; rfl
+    rw [Int.negSucc_eq, Rat.zpow_neg, this, Rat.mul_def']
+    simp only [Rat.num_mkRat, Rat.den_mkRat]
+    simp only [natCast_pow, natCast_ofNat, den_inv, num_pow, num_ofNat, Int.natAbs_pow,
+      Int.reduceAbs, num_inv, den_pow, den_ofNat, Nat.one_pow, Int.cast_ofNat_Int, Int.mul_one]
+    have : ¬ (2 ^ (prec + 1) : Int) = 0 := NeZero.out
+    simp only [if_neg this]
+    have : (2 ^ (prec + 1) : Int).sign = 1 := by simpa using Int.pow_pos (by decide)
+    simp only [this]
+    have : x.den * 2 ^ (prec + 1) = 0 ↔ x.den = 0 := by
+      rw [Nat.mul_eq_zero]
+      simp_all
+    simp only [this, Int.mul_one]
+    split
+    · simp_all
+    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+      congr 1
+      rw [Int.natCast_ediv, Int.mul_ediv_cancel']
+      · simp
+      · rw [Int.natCast_dvd_natCast]
+        apply gcd_dvd_left
+
+theorem toRat_toDyadic_le {x : Rat} {prec : Int} : (x.toDyadic prec).toRat ≤ x := by
+  rw [toRat_toDyadic]
+  have : (x * 2 ^ prec).floor ≤ x * 2 ^ prec := Rat.floor_le _
+  apply Rat.le_of_mul_le_mul_right (c := 2 ^ prec)
+  rw [Rat.div_mul_cancel]
+  exact this
+  · apply Rat.ne_of_gt (Rat.zpow_pos (by decide))
+  · exact Rat.zpow_pos (by decide)
+
+theorem lt_toRat_toDyadic_add {x : Rat} {prec : Int} :
+    x < (x.toDyadic prec + ofIntWithPrec 1 prec).toRat := by
+  rw [toRat_add, toRat_toDyadic, toRat_ofIntWithPrec_eq_mul_two_pow]
+  have := Rat.lt_floor_add_one (x * 2 ^ prec)
+  rw [Rat.zpow_neg, Rat.div_def, ← Rat.add_mul]
+  apply Rat.lt_of_mul_lt_mul_right (c := 2 ^ prec)
+  rw [Rat.mul_assoc, Rat.inv_mul_cancel, Rat.mul_one]
+  exact mod_cast this
+  · apply Rat.ne_of_gt (Rat.zpow_pos (by decide))
+  · exact Rat.zpow_nonneg (by decide)
+
+-- TODO: `x.toDyadic prec` is the unique dyadic with the given precision satisfying the two inequalities above.
+
+end Rat
+
+namespace Dyadic
+
 /--
 Rounds a dyadic rational `x` down to the greatest dyadic number with precision at most `prec`
 which is less than or equal to `x`.
@@ -479,10 +566,11 @@ theorem toDyadic_toRat (x : Dyadic) (prec : Int) :
     rw [this]
     cases h : k - prec
     · simp
-    · simp
+    · simp only [Int.neg_negSucc, Int.natCast_add, Int.cast_ofNat_Int, Int.toNat_natCast_add_one,
+        Int.toNat_negSucc, Int.shiftRight_zero]
       rw [Int.negSucc_eq, Int.eq_neg_comm, Int.neg_sub, eq_comm, Int.sub_eq_iff_eq_add] at h
-      simp only [Int.neg_negSucc, h, ← Int.natCast_add_one, Int.add_comm _ k,
-        Nat.succ_eq_add_one, Int.toNat_natCast, ofIntWithPrec_shiftLeft_add, ofOdd_eq_ofIntWithPrec]
+      simp only [h, ← Int.natCast_add_one, Int.add_comm _ k, ofIntWithPrec_shiftLeft_add,
+        ofOdd_eq_ofIntWithPrec]
 
 theorem toRat_inj {x y : Dyadic} : x.toRat = y.toRat ↔ x = y := by
   refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
@@ -578,7 +666,7 @@ theorem blt_eq_false_iff : blt x y = false ↔ ble y x = true := by
     rcases k₁ - k₂ with (_ | _) | _
     · simp
     · simp [← Int.negSucc_eq]
-    · simp only [Int.neg_negSucc, succ_eq_add_one, decide_eq_false_iff_not, Int.not_lt,
+    · simp only [Int.neg_negSucc, decide_eq_false_iff_not, Int.not_lt,
         decide_eq_true_eq]
 
 theorem ble_iff_toRat : ble x y ↔ x.toRat ≤ y.toRat := by
diff --git a/src/Init/Data/Dyadic/Inv.lean b/src/Init/Data/Dyadic/Inv.lean
new file mode 100644
index 0000000000..3f9c44eca1
--- /dev/null
+++ b/src/Init/Data/Dyadic/Inv.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+prelude
+import Init.Data.Dyadic.Basic
+import Init.Data.Dyadic.Round
+import Init.Grind.Ordered.Ring
+
+/-!
+# Inversion for dyadic numbers
+-/
+
+namespace Dyadic
+
+/--
+Inverts a dyadic number at a given (maximum) precision.
+Returns the greatest dyadic number with precision at most `prec` which is less than or equal to `1/x`.
+For `x = 0`, returns `0`.
+-/
+def invAtPrec (x : Dyadic) (prec : Int) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | _ => x.toRat.inv.toDyadic prec
+
+/-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`. -/
+theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
+    invAtPrec x prec * x ≤ 1 := by
+  rw [le_iff_toRat]
+  rw [toRat_mul]
+  rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
+  unfold invAtPrec
+  cases x with
+  | zero =>
+    exfalso
+    contradiction
+  | ofOdd n k hn =>
+    simp only
+    have h_le : ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat ≤ (ofOdd n k hn).toRat.inv := Rat.toRat_toDyadic_le
+    have h_pos : 0 ≤ (ofOdd n k hn).toRat := by
+      rw [lt_iff_toRat, toRat_zero] at hx
+      exact Rat.le_of_lt hx
+    calc ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat * (ofOdd n k hn).toRat
+        ≤ (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := Rat.mul_le_mul_of_nonneg_right h_le h_pos
+      _ = 1 := by
+        apply Rat.inv_mul_cancel
+        rw [lt_iff_toRat, toRat_zero] at hx
+        exact Rat.ne_of_gt hx
+
+/-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`. -/
+theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
+    1 < (invAtPrec x prec + ofIntWithPrec 1 prec) * x := by
+  rw [lt_iff_toRat]
+  rw [toRat_mul]
+  rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
+  unfold invAtPrec
+  cases x with
+  | zero =>
+    exfalso
+    contradiction
+  | ofOdd n k hn =>
+    simp only
+    have h_le : (ofOdd n k hn).toRat.inv < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat :=
+      Rat.lt_toRat_toDyadic_add
+    have h_pos : 0 < (ofOdd n k hn).toRat := by
+      rwa [lt_iff_toRat, toRat_zero] at hx
+    calc
+      1 = (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := by
+        symm
+        apply Rat.inv_mul_cancel
+        rw [lt_iff_toRat, toRat_zero] at hx
+        exact Rat.ne_of_gt hx
+      _ < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat * (ofOdd n k hn).toRat :=
+           Rat.mul_lt_mul_of_pos_right h_le h_pos
+
+-- TODO: `invAtPrec` is the unique dyadic with the given precision satisfying the two inequalities above.
+
+end Dyadic
diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean
index b481109bff..987d10c511 100644
--- a/src/Init/Data/Int/DivMod/Bootstrap.lean
+++ b/src/Init/Data/Int/DivMod/Bootstrap.lean
@@ -97,7 +97,7 @@ theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n
 
 /-! ### mod definitions -/
 
-theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
+theorem emod_add_mul_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | ofNat m, -[n+1] => by
     change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
@@ -111,19 +111,35 @@ where
       ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
     exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
 
-/-- Variant of `emod_add_ediv` with the multiplication written the other way around. -/
-theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
-  rw [Int.mul_comm]; exact emod_add_ediv ..
+@[deprecated emod_add_mul_ediv (since := "2025-09-01")]
+def emod_add_ediv := @emod_add_mul_ediv
 
-theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
-  rw [Int.add_comm]; exact emod_add_ediv ..
+theorem emod_add_ediv_mul (a b : Int) : a % b + a / b * b = a := by
+  rw [Int.mul_comm]; exact emod_add_mul_ediv ..
 
-/-- Variant of `ediv_add_emod` with the multiplication written the other way around. -/
-theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
-  rw [Int.mul_comm]; exact ediv_add_emod ..
+@[deprecated emod_add_ediv_mul (since := "2025-09-01")]
+def emod_add_ediv' := @emod_add_ediv_mul
+
+theorem mul_ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
+  rw [Int.add_comm]; exact emod_add_mul_ediv ..
+
+@[deprecated mul_ediv_add_emod (since := "2025-09-01")]
+def ediv_add_emod := @mul_ediv_add_emod
+
+theorem ediv_mul_add_emod (a b : Int) : a / b * b + a % b = a := by
+  rw [Int.mul_comm]; exact mul_ediv_add_emod ..
+
+@[deprecated ediv_mul_add_emod (since := "2025-09-01")]
+def ediv_add_emod' := @ediv_mul_add_emod
 
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
-  rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
+  rw [← Int.add_sub_cancel (a % b), emod_add_mul_ediv]
+
+theorem mul_ediv_self (a b : Int) : b * (a / b) = a - a % b := by
+  rw [emod_def, Int.sub_sub_self]
+
+theorem ediv_mul_self (a b : Int) : a / b * b = a - a % b := by
+  rw [Int.mul_comm, emod_def, Int.sub_sub_self]
 
 /-! ### `/` ediv -/
 
@@ -226,7 +242,7 @@ theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
 
 @[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
   have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
-  rwa [Int.add_right_comm, emod_add_ediv] at this
+  rwa [Int.add_right_comm, emod_add_mul_ediv] at this
 
 @[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
   rw [Int.add_comm, emod_add_emod, Int.add_comm]
@@ -252,7 +268,7 @@ theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔
 
 theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   conv => lhs; rw [
-    ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
+    ← emod_add_mul_ediv a n, ← emod_add_ediv_mul b n, Int.add_mul, Int.mul_add, Int.mul_add,
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
     ← Int.mul_assoc, add_mul_emod_self_right]
 
@@ -261,7 +277,7 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
 
 @[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
     (h : m ∣ k) : (n % k) % m = n % m := by
-  conv => rhs; rw [← emod_add_ediv n k]
+  conv => rhs; rw [← emod_add_mul_ediv n k]
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
 
@@ -275,7 +291,7 @@ theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
 /-! ### properties of `/` and `%` -/
 
 theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
-  have := emod_add_ediv a b; rwa [H, Int.zero_add] at this
+  have := emod_add_mul_ediv a b; rwa [H, Int.zero_add] at this
 
 theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
   rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]
@@ -326,11 +342,11 @@ theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a :
 theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
   calc k * (x / k)
     _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
-    _ = x                   := ediv_add_emod _ _
+    _ = x                   := mul_ediv_add_emod _ _
 
 theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
   calc x
-    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
+    _ = k * (x / k) + x % k := (mul_ediv_add_emod _ _).symm
     _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
 
 /-! ### bmod -/
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index b9f3420c5b..56e01f61be 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -334,7 +334,7 @@ theorem fdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.fdiv b = a / b := by
 
 /-! ### mod definitions -/
 
-theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
+theorem tmod_add_mul_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
   | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
   | ofNat m, -[n+1] => by
     change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
@@ -351,21 +351,37 @@ theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
     rw [Int.neg_mul, ← Int.neg_add]
     exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
 
-theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
-  rw [Int.add_comm]; apply tmod_add_tdiv ..
+@[deprecated tmod_add_mul_tdiv (since := "2025-09-01")]
+def tmod_add_tdiv := @tmod_add_mul_tdiv
 
-/-- Variant of `tmod_add_tdiv` with the multiplication written the other way around. -/
-theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m := by
-  rw [Int.mul_comm]; apply tmod_add_tdiv
+theorem mul_tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
+  rw [Int.add_comm]; apply tmod_add_mul_tdiv ..
 
-/-- Variant of `tdiv_add_tmod` with the multiplication written the other way around. -/
-theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m := by
-  rw [Int.mul_comm]; apply tdiv_add_tmod
+@[deprecated mul_tdiv_add_tmod (since := "2025-09-01")]
+def tdiv_add_tmod := @mul_tdiv_add_tmod
+
+theorem tmod_add_tdiv_mul (m k : Int) : tmod m k + m.tdiv k * k = m := by
+  rw [Int.mul_comm]; apply tmod_add_mul_tdiv
+
+@[deprecated tmod_add_tdiv_mul (since := "2025-09-01")]
+def tmod_add_tdiv' := @tmod_add_mul_tdiv
+
+theorem tdiv_mul_add_tmod (m k : Int) : m.tdiv k * k + tmod m k = m := by
+  rw [Int.mul_comm]; apply mul_tdiv_add_tmod
+
+@[deprecated tdiv_mul_add_tmod (since := "2025-09-01")]
+def tdiv_add_tmod' := @tdiv_mul_add_tmod
 
 theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b := by
-  rw [← Int.add_sub_cancel (tmod a b), tmod_add_tdiv]
+  rw [← Int.add_sub_cancel (tmod a b), tmod_add_mul_tdiv]
 
-theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
+theorem mul_tdiv_self (a b : Int) : b * (a.tdiv b) = a - a.tmod b := by
+  rw [tmod_def, Int.sub_sub_self]
+
+theorem tdiv_mul_self (a b : Int) : a.tdiv b * b = a - a.tmod b := by
+  rw [Int.mul_comm, tmod_def, Int.sub_sub_self]
+
+theorem fmod_add_mul_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
   | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
   | succ _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | succ m, -[n+1] => by
@@ -382,19 +398,35 @@ theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
     change -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
     rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
 
-/-- Variant of `fmod_add_fdiv` with the multiplication written the other way around. -/
-theorem fmod_add_fdiv' (a b : Int) : a.fmod b + (a.fdiv b) * b = a := by
-  rw [Int.mul_comm]; exact fmod_add_fdiv ..
+@[deprecated fmod_add_mul_fdiv (since := "2025-09-01")]
+def fmod_add_fdiv := @fmod_add_mul_fdiv
 
-theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
-  rw [Int.add_comm]; exact fmod_add_fdiv ..
+theorem fmod_add_fdiv_mul (a b : Int) : a.fmod b + (a.fdiv b) * b = a := by
+  rw [Int.mul_comm]; exact fmod_add_mul_fdiv ..
 
-/-- Variant of `fdiv_add_fmod` with the multiplication written the other way around. -/
-theorem fdiv_add_fmod' (a b : Int) : (a.fdiv b) * b + a.fmod b = a := by
-  rw [Int.mul_comm]; exact fdiv_add_fmod ..
+@[deprecated fmod_add_fdiv_mul (since := "2025-09-01")]
+def fmod_add_fdiv' := @fmod_add_fdiv_mul
+
+theorem mul_fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
+  rw [Int.add_comm]; exact fmod_add_mul_fdiv ..
+
+@[deprecated mul_fdiv_add_fmod (since := "2025-09-01")]
+def fdiv_add_fmod := @mul_fdiv_add_fmod
+
+theorem fdiv_mul_add_fmod (a b : Int) : (a.fdiv b) * b + a.fmod b = a := by
+  rw [Int.mul_comm]; exact mul_fdiv_add_fmod ..
+
+@[deprecated mul_fdiv_add_fmod (since := "2025-09-01")]
+def fdiv_add_fmod' := @mul_fdiv_add_fmod
 
 theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
-  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]
+  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_mul_fdiv]
+
+theorem mul_fdiv_self (a b : Int) : b * (a.fdiv b) = a - a.fmod b := by
+  rw [fmod_def, Int.sub_sub_self]
+
+theorem fdiv_mul_self (a b : Int) : a.fdiv b * b = a - a.fmod b := by
+  rw [Int.mul_comm, fmod_def, Int.sub_sub_self]
 
 /-! ### mod equivalences  -/
 
@@ -773,7 +805,7 @@ protected theorem ediv_emod_unique {a b r q : Int} (h : 0 < b) :
     a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b := by
   constructor
   · intro ⟨rfl, rfl⟩
-    exact ⟨emod_add_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩
+    exact ⟨emod_add_mul_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩
   · intro ⟨rfl, hz, hb⟩
     constructor
     · rw [Int.add_mul_ediv_left r q (Int.ne_of_gt h), ediv_eq_zero_of_lt hz hb]
@@ -797,7 +829,7 @@ theorem neg_ediv {a b : Int} : (-a) / b = -(a / b) - if b ∣ a then 0 else b.si
   if hb : b = 0 then
     simp [hb]
   else
-    conv => lhs; rw [← ediv_add_emod a b]
+    conv => lhs; rw [← mul_ediv_add_emod a b]
     rw [Int.neg_add, ← Int.mul_neg, mul_add_ediv_left _ _ hb, Int.add_comm]
     split <;> rename_i h
     · rw [emod_eq_zero_of_dvd h]
@@ -1087,6 +1119,10 @@ theorem emod_natAbs_of_neg {x : Int} (h : x < 0) {n : Nat} (w : n ≠ 0) :
 protected theorem ediv_mul_le (a : Int) {b : Int} (H : b ≠ 0) : a / b * b ≤ a :=
   Int.le_of_sub_nonneg <| by rw [Int.mul_comm, ← emod_def]; apply emod_nonneg _ H
 
+protected theorem lt_ediv_mul (a : Int) {b : Int} (H : 0 < b) : a - b < a / b * b := by
+  rw [ediv_mul_self, Int.sub_lt_sub_left_iff]
+  exact emod_lt_of_pos a H
+
 theorem le_of_mul_le_mul_left {a b c : Int} (w : a * b ≤ a * c) (h : 0 < a) : b ≤ c := by
   have w := Int.sub_nonneg_of_le w
   rw [← Int.mul_sub] at w
@@ -1177,9 +1213,9 @@ theorem ediv_eq_iff_of_pos {k x y : Int} (h : 0 < k) : x / k = y ↔ y * k ≤ x
 theorem add_ediv_of_pos {a b c : Int} (h : 0 < c) :
     (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
   have h' : c ≠ 0 := by omega
-  conv => lhs; rw [← Int.ediv_add_emod a c]
+  conv => lhs; rw [← Int.mul_ediv_add_emod a c]
   rw [Int.add_assoc, Int.mul_add_ediv_left _ _ h']
-  conv => lhs; rw [← Int.ediv_add_emod b c]
+  conv => lhs; rw [← Int.mul_ediv_add_emod b c]
   rw [Int.add_comm (a % c), Int.add_assoc, Int.mul_add_ediv_left _ _ h',
     ← Int.add_assoc, Int.add_comm (b % c)]
   congr
@@ -1210,7 +1246,7 @@ theorem not_dvd_iff_lt_mul_succ (m : Int) (hn : 0 < n) :
     ¬n ∣ m ↔ (∃ k, n * k < m ∧ m < n * (k + 1)) := by
   refine ⟨fun h ↦ ?_, ?_⟩
   · rw [dvd_iff_emod_eq_zero, ← Ne] at h
-    rw [← emod_add_ediv m n]
+    rw [← emod_add_mul_ediv m n]
     refine ⟨m / n, Int.lt_add_of_pos_left _ ?_, ?_⟩
     · have := emod_nonneg m (Int.ne_of_gt hn)
       omega
@@ -1485,7 +1521,7 @@ theorem sign_tmod (a b : Int) : sign (tmod a b) = if b ∣ a then 0 else sign a
 -- Analogues of statements about `ediv` and `emod` from `Bootstrap.lean`
 
 theorem mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * (a.tdiv b) = a := by
-  have := tmod_add_tdiv a b; rwa [H, Int.zero_add] at this
+  have := tmod_add_mul_tdiv a b; rwa [H, Int.zero_add] at this
 
 theorem tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a := by
   rw [Int.mul_comm, mul_tdiv_cancel_of_tmod_eq_zero H]
@@ -2210,7 +2246,7 @@ theorem fmod_add_cancel_right {m n k : Int} (i) : (m + i).fmod n = (k + i).fmod
 
 theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n := by
   conv => lhs; rw [
-    ← fmod_add_fdiv a n, ← fmod_add_fdiv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
+    ← fmod_add_mul_fdiv a n, ← fmod_add_fdiv_mul b n, Int.add_mul, Int.mul_add, Int.mul_add,
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_fmod_self_left,
     ← Int.mul_assoc, add_mul_fmod_self_right]
 
@@ -2219,7 +2255,7 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n :
 
 @[simp] theorem fmod_fmod_of_dvd (n : Int) {m k : Int}
     (h : m ∣ k) : (n.fmod k).fmod m = n.fmod m := by
-  conv => rhs; rw [← fmod_add_fdiv n k]
+  conv => rhs; rw [← fmod_add_mul_fdiv n k]
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left]
 
@@ -2249,7 +2285,7 @@ theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a :=
 -- Analogues of properties of `ediv` and `emod` from `Bootstrap.lean`
 
 theorem mul_fdiv_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) : b * (a.fdiv b) = a := by
-  have := fmod_add_fdiv a b; rwa [H, Int.zero_add] at this
+  have := fmod_add_mul_fdiv a b; rwa [H, Int.zero_add] at this
 
 theorem fdiv_mul_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) : (a.fdiv b) * b= a := by
   rw [Int.mul_comm, mul_fdiv_cancel_of_fmod_eq_zero H]
@@ -2491,9 +2527,9 @@ theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
       ite_self]
   · dsimp only
     split
-    · exact ediv_add_emod x m
+    · exact mul_ediv_add_emod x m
     · rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm m, Int.sub_add_cancel]
-      exact ediv_add_emod x m
+      exact mul_ediv_add_emod x m
 
 theorem bmod_add_bdiv (x : Int) (m : Nat) : bmod x m + m * bdiv x m = x := by
   rw [Int.add_comm]; exact bdiv_add_bmod x m
@@ -2750,7 +2786,7 @@ theorem le_bmod {x : Int} {m : Nat} (h : 0 < m) : - (m/2) ≤ Int.bmod x m := by
     · exact Int.ne_of_gt (natCast_pos.mpr h)
   · simp [Int.not_lt] at w
     refine Int.le_trans ?_ (Int.sub_le_sub_right w _)
-    rw [← ediv_add_emod m 2]
+    rw [← mul_ediv_add_emod m 2]
     generalize (m : Int) / 2 = q
     generalize h : (m : Int) % 2 = r at *
     rcases v with rfl | rfl
@@ -2911,7 +2947,7 @@ theorem neg_bmod {a : Int} {b : Nat} :
           simp only [gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left, Int.natCast_mul,
             cast_ofNat_Int, Int.not_lt] at *
           rw [Int.mul_dvd_mul_iff_left (by omega)]
-          have := ediv_add_emod a (2 * c)
+          have := mul_ediv_add_emod a (2 * c)
           rw [(by omega : a % (2 * c) = c)] at this
           rw [← this]
           apply Int.dvd_add _ (by simp)
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index de157d3c1b..3b86b7a0b8 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -40,7 +40,7 @@ theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 
 theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
 theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
-theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
+@[simp] theorem neg_negSucc (n : Nat) : -(-[n+1]) = ((n + 1 : Nat) : Int) := rfl
 
 theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 
diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 38ece53696..e1843afcba 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -247,7 +247,7 @@ def cmod (a b : Int) : Int :=
 
 theorem cdiv_add_cmod (a b : Int) : b*(cdiv a b) + cmod a b = a := by
   unfold cdiv cmod
-  have := Int.ediv_add_emod (-a) b
+  have := Int.mul_ediv_add_emod (-a) b
   have := congrArg (Neg.neg) this
   simp at this
   conv => rhs; rw[← this]
@@ -272,7 +272,7 @@ private abbrev div_mul_cancel_of_mod_zero :=
 theorem cdiv_eq_div_of_divides {a b : Int} (h : a % b = 0) : a/b = cdiv a b := by
   replace h := div_mul_cancel_of_mod_zero h
   have hz : a % b = 0 := by
-    have := Int.ediv_add_emod a b
+    have := Int.mul_ediv_add_emod a b
     conv at this => rhs; rw [← Int.add_zero a]
     rw [Int.mul_comm, h] at this
     exact Int.add_left_cancel this
@@ -1753,7 +1753,7 @@ theorem cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b :
   intros; subst b p'; simp; assumption
 
 private theorem one_emod_eq_one {a : Int} (h : a > 1) : 1 % a = 1 := by
-  have aux₁ := Int.ediv_add_emod 1 a
+  have aux₁ := Int.mul_ediv_add_emod 1 a
   have : 1 / a = 0 := Int.ediv_eq_zero_of_lt (by decide) h
   simp [this] at aux₁
   assumption
@@ -1780,7 +1780,7 @@ private theorem ex_of_dvd {α β a b d x : Int}
     rw [Int.mul_emod, aux₁, Int.one_mul, Int.emod_emod] at this
     assumption
   have : x = (x / d)*d + (- α * b) % d := by
-    conv => lhs; rw [← Int.ediv_add_emod x d]
+    conv => lhs; rw [← Int.mul_ediv_add_emod x d]
     rw [Int.mul_comm, this]
   exists x / d
 
@@ -1863,7 +1863,7 @@ theorem cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (α β :
   exact cooper_unsat' h₁ h₂ h₃ h₄ h₅ h₆
 
 theorem ediv_emod (x y : Int) : -1 * x + y * (x / y) + x % y = 0 := by
-  rw [Int.add_assoc, Int.ediv_add_emod x y, Int.add_comm]
+  rw [Int.add_assoc, Int.mul_ediv_add_emod x y, Int.add_comm]
   simp
   rw [Int.add_neg_eq_sub, Int.sub_self]
 
diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean
index 4a2061820b..22c38835f8 100644
--- a/src/Init/Data/Int/Order.lean
+++ b/src/Init/Data/Int/Order.lean
@@ -701,10 +701,13 @@ theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
   | (_+1:Nat) => Nat.add_zero _
   | -[_+1] => Nat.zero_add _
 
-@[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
+@[simp] theorem toNat_neg_natCast : ∀ n : Nat, (-(n : Int)).toNat = 0
   | 0 => rfl
   | _+1 => rfl
 
+@[deprecated toNat_neg_natCast (since := "2025-08-29")]
+theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0 := toNat_neg_natCast
+
 /-! ### toNat? -/
 
 theorem mem_toNat? : ∀ {a : Int} {n : Nat}, toNat? a = some n ↔ a = n
diff --git a/src/Init/Data/Rat/Basic.lean b/src/Init/Data/Rat/Basic.lean
index 321f6cf9de..c2e8d20a67 100644
--- a/src/Init/Data/Rat/Basic.lean
+++ b/src/Init/Data/Rat/Basic.lean
@@ -150,6 +150,9 @@ instance : LE Rat := ⟨fun a b => b.blt a = false⟩
 instance (a b : Rat) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (_ = false))
 
+instance : Min Rat := minOfLe
+instance : Max Rat := maxOfLe
+
 /-- Multiplication of rational numbers. (This definition is `@[irreducible]` because you don't
 want to unfold it. Use `Rat.mul_def` instead.) -/
 @[irreducible] protected def mul (a b : Rat) : Rat :=
diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean
index 97cfa428fc..4ce6b20d80 100644
--- a/src/Init/Data/Rat/Lemmas.lean
+++ b/src/Init/Data/Rat/Lemmas.lean
@@ -7,6 +7,7 @@ module
 prelude
 
 public import Init.Data.Rat.Basic
+public import Init.Data.Int.Gcd
 import Init.Data.Int.Bitwise.Lemmas
 
 @[expose] public section
@@ -41,6 +42,14 @@ theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
       reduced := normalize.reduced den_nz rfl } := by
   simp only [normalize, maybeNormalize_eq, Int.divExact_eq_ediv]
 
+@[simp]
+theorem num_normalize {num den} (den_nz) : (normalize num den den_nz).num = num / num.natAbs.gcd den := by
+  simp [normalize_eq]
+
+@[simp]
+theorem den_normalize {num den} (den_nz) : (normalize num den den_nz).den = den / num.natAbs.gcd den := by
+  simp [normalize_eq]
+
 @[simp] theorem normalize_zero (nz) : normalize 0 d nz = 0 := by
   simp [normalize, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl
 
@@ -111,6 +120,14 @@ theorem mkRat_num_den (z : d ≠ 0) (h : mkRat n d = ⟨n', d', z', c⟩) :
 
 theorem mkRat_def (n d) : mkRat n d = if d0 : d = 0 then 0 else normalize n d d0 := rfl
 
+theorem num_mkRat (n d) : (mkRat n d).num = if d = 0 then 0 else n / d.gcd n.natAbs := by
+  rw [mkRat_def]
+  split <;> simp [Nat.gcd_comm]
+
+theorem den_mkRat (n d) : (mkRat n d).den = if d = 0 then 1 else d / d.gcd n.natAbs := by
+  rw [mkRat_def]
+  split <;> simp [Nat.gcd_comm]
+
 @[simp]
 theorem mkRat_self (a : Rat) : mkRat a.num a.den = a := by
   rw [← normalize_eq_mkRat a.den_nz, normalize_self]
@@ -199,6 +216,27 @@ theorem divInt_num_den (z : d ≠ 0) (h : n /. d = ⟨n', d', z', c⟩) :
     rw [← Int.neg_inj, Int.neg_neg] at h₂
     simp [Int.natCast_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]
 
+theorem num_divInt (a b : Int) : (a /. b).num = b.sign * a / b.gcd a := by
+  rw [divInt.eq_def]
+  simp only [inline, Nat.succ_eq_add_one]
+  split <;> rename_i d
+  · simp only [num_mkRat, Int.ofNat_eq_coe]
+    split <;> rename_i h
+    · simp_all
+    · rw [Int.sign_natCast_of_ne_zero h, Int.one_mul, Int.gcd]
+      simp
+  · simp [Int.gcd, Nat.gcd_comm]
+
+theorem den_divInt (a b : Int) : (a /. b).den = if b = 0 then 1 else b.natAbs / b.gcd a := by
+  rw [divInt.eq_def]
+  simp only [inline, Nat.succ_eq_add_one]
+  split <;> rename_i d
+  · simp only [den_mkRat, Int.ofNat_eq_coe, Int.natAbs_cast]
+    split <;> rename_i h
+    · simp_all
+    · simp [if_neg (by omega), Int.gcd]
+  · simp [Int.gcd, Nat.gcd_comm]
+
 /-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
 numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`. -/
 @[elab_as_elim]
@@ -225,8 +263,11 @@ def numDenCasesOn''.{u} {C : Rat → Sort u} (a : Rat)
 @[simp] theorem ofInt_num : (ofInt n : Rat).num = n := rfl
 @[simp] theorem ofInt_den : (ofInt n : Rat).den = 1 := rfl
 
-@[simp] theorem num_ofNat : (OfNat.ofNat n : Rat).num = OfNat.ofNat n := rfl
-@[simp] theorem den_ofNat : (OfNat.ofNat n : Rat).den = 1 := rfl
+@[simp] theorem num_ofNat : (no_index (OfNat.ofNat n : Rat)).num = OfNat.ofNat n := rfl
+@[simp] theorem den_ofNat : (no_index (OfNat.ofNat n : Rat)).den = 1 := rfl
+
+@[simp] theorem num_natCast (n : Nat) : (n : Rat).num = n := rfl
+@[simp] theorem den_natCast (n : Nat) : (n : Rat).den = 1 := rfl
 
 @[deprecated num_ofNat (since := "2025-08-22")]
 abbrev ofNat_num := @num_ofNat
@@ -426,6 +467,22 @@ theorem inv_def (a : Rat) : a⁻¹ = (a.den : Int) /. a.num := by
     apply (num_divInt_den _).symm.trans
     simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]
 
+@[simp] theorem num_inv (a : Rat) : (a⁻¹).num = a.num.sign * a.den := by
+  simp only [inv_def]
+  rw [num_divInt]
+  have := a.reduced
+  dsimp [Nat.Coprime] at this
+  simp [Int.gcd, this]
+
+@[simp] theorem den_inv (a : Rat) : (a⁻¹).den = if a.num = 0 then 1 else a.num.natAbs := by
+  simp only [inv_def]
+  rw [den_divInt]
+  split
+  · rfl
+  · have := a.reduced
+    dsimp [Nat.Coprime] at this
+    simp [Int.gcd, this]
+
 @[simp] protected theorem inv_zero : (0 : Rat)⁻¹ = 0 := by
   change Rat.inv 0 = 0; unfold Rat.inv; rfl
 
@@ -488,6 +545,9 @@ theorem pow_def (q : Rat) (n : Nat) :
     q ^ n = ⟨q.num ^ n, q.den ^ n, by simp [q.den_nz],
       by rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩ := rfl
 
+@[simp] theorem num_pow (q : Rat) (n : Nat) : (q ^ n).num = q.num ^ n := rfl
+@[simp] theorem den_pow (q : Rat) (n : Nat) : (q ^ n).den = q.den ^ n := rfl
+
 @[simp] protected theorem pow_zero (q : Rat) : q ^ 0 = 1 := rfl
 
 protected theorem pow_succ (q : Rat) (n : Nat) : q ^ (n + 1) = q ^ n * q := by
@@ -700,6 +760,17 @@ protected theorem mul_pos {a b : Rat} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := b
   refine Rat.lt_of_le_of_ne (Rat.mul_nonneg (Rat.le_of_lt ha) (Rat.le_of_lt hb)) ?_
   simp [eq_comm, Rat.mul_eq_zero, Rat.ne_of_gt ha, Rat.ne_of_gt hb]
 
+protected theorem mul_le_mul_of_nonneg_left {a b c : Rat} (ha : a ≤ b) (hc : 0 ≤ c) :
+    c * a ≤ c * b := by
+  rw [Rat.le_iff_sub_nonneg, Rat.sub_eq_add_neg] at ha ⊢
+  rw [← Rat.mul_neg, ← Rat.mul_add]
+  exact Rat.mul_nonneg hc ha
+
+protected theorem mul_le_mul_of_nonneg_right {a b c : Rat} (ha : a ≤ b) (hc : 0 ≤ c) :
+    a * c ≤ b * c := by
+  rw [Rat.mul_comm _ c, Rat.mul_comm _ c]
+  exact Rat.mul_le_mul_of_nonneg_left ha hc
+
 protected theorem mul_lt_mul_of_pos_left {a b c : Rat} (ha : a < b) (hc : 0 < c) :
     c * a < c * b := by
   rw [Rat.lt_iff_sub_pos, Rat.sub_eq_add_neg] at ha ⊢
@@ -935,3 +1006,63 @@ theorem intCast_nonpos {a : Int} :
 theorem intCast_neg_iff {a : Int} :
     (a : Rat) < 0 ↔ a < 0 :=
   Rat.intCast_lt_intCast
+
+theorem floor_def (a : Rat) : a.floor = a.num / a.den := by
+  rw [Rat.floor]
+  split <;> simp_all
+
+@[simp]
+theorem floor_intCast (a : Int) : (a : Rat).floor = a := by
+  simp [floor_def]
+
+theorem floor_monotone {a b : Rat} (h : a ≤ b) : a.floor ≤ b.floor := by
+  rw [floor_def, floor_def]
+  rw [Rat.le_iff] at h
+  rw [Int.ediv_le_iff_le_mul (by have := a.den_nz; omega),
+    ← Int.mul_lt_mul_right (a := b.den) (by have := b.den_nz; omega)]
+  apply Int.lt_of_le_of_lt h
+  conv =>
+    rhs; congr; congr; rfl
+    rw [← Int.one_mul a.den]
+  rw [← Int.add_mul, Int.mul_right_comm,
+    Int.mul_lt_mul_right (a := a.den) (by have := a.den_nz; omega),
+    Int.add_mul, Int.one_mul, ← Int.sub_lt_iff]
+  exact Int.lt_ediv_mul b.num (b := b.den) (by have := b.den_nz; omega)
+
+theorem floor_le (a : Rat) : (a.floor : Rat) ≤ a := by
+  rw [floor_def, Rat.le_iff, num_intCast, den_intCast, Int.cast_ofNat_Int, Int.mul_one]
+  apply Int.ediv_mul_le _ (by simpa using a.den_nz)
+
+theorem lt_floor_add_one (a : Rat) : a < ((a.floor + 1 : Int): Rat) := by
+  rw [floor_def, Rat.lt_iff]
+  have : a.num / ↑a.den + 1 = (a.num + ↑a.den) / ↑a.den := by
+    rw [Int.add_ediv_of_dvd_right] <;> simp [a.den_nz]
+  simp [this]
+  simpa using Int.lt_ediv_mul (a.num + a.den) (b := a.den) (by have := a.den_nz; omega)
+
+theorem le_floor_iff {x : Int} {a : Rat} : x ≤ a.floor ↔ (x : Rat) ≤ a := by
+  constructor
+  · intro h
+    rw [← intCast_le_intCast] at h
+    exact Rat.le_trans h (floor_le a)
+  · intro h
+    simpa using floor_monotone h
+
+theorem floor_lt_iff {a : Rat} {x : Int} : a.floor < x ↔ a < (x : Rat) := by
+  rw [← Decidable.not_iff_not, Int.not_lt, le_floor_iff, Rat.not_lt]
+
+theorem ceil_eq_neg_floor_neg (a : Rat) : a.ceil = -((-a).floor) := by
+  rw [Rat.ceil, Rat.floor]
+  simp only [neg_den, neg_num]
+  split
+  · simp
+  · rw [Int.neg_ediv, if_neg, Int.sign_eq_one_of_pos, Int.neg_sub, Int.sub_neg, Int.add_comm]
+    · have := a.den_nz; omega
+    · intro h
+      rw [Int.ofNat_dvd_left] at h
+      exact Nat.not_coprime_of_dvd_of_dvd (by have := a.den_nz; omega) h (Nat.dvd_refl _) a.reduced
+
+@[simp]
+theorem ceil_intCast (a : Int) : (a : Rat).ceil = a := rfl
+
+-- TODO: reproduce the `floor` inequalities above for `ceil`
diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean
index f2a8838f46..827a1956d5 100644
--- a/src/Init/Grind/Ring/Poly.lean
+++ b/src/Init/Grind/Ring/Poly.lean
@@ -1534,7 +1534,7 @@ theorem diseq0_to_eq {α} [Field α] (a : α) : a ≠ 0 → a*a⁻¹ = 1 := by
 
 private theorem of_mod_eq_0 {α} [CommRing α] {a : Int} {c : Nat} : Int.cast c = (0 : α) → a % c = 0 → (a : α) = 0 := by
   intro h h'
-  have := Int.ediv_add_emod a ↑c
+  have := Int.mul_ediv_add_emod a ↑c
   rw [h', Int.add_zero] at this
   replace this := congrArg (Int.cast (R := α)) this
   rw [Ring.intCast_mul] at this
diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index 3f2cb12d2f..024d797ba1 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -124,7 +124,7 @@ theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a :=
   split <;> rename_i n
   · simp only [Int.ofNat_eq_coe]
     rw [if_pos (Int.natCast_nonneg n)]
-  · simp; rfl
+  · simp
 
 theorem natAbs_dichotomy {a : Int} : 0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a := by
   by_cases h : 0 ≤ a