avoid where finally for now

Let's not have the confusion of interpreting `toRat_of_eq_mkRat`
as `_ = mkRat _ _ -> toRat _ = _`

src/Init/Data.lean

@@ -51,5 +51,6 @@ public import Init.Data.Range.Polymorphic
 public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
+public import Init.Data.Dyadic
 
 public section

src/Init/Data/Dyadic.lean

@@ -0,0 +1,10 @@
+/-
+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
+
+public import Init.Data.Dyadic.Basic
+public import Init.Data.Dyadic.Instances

src/Init/Data/Dyadic/Basic.lean

@@ -0,0 +1,630 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Robin Arnez
+-/
+module
+
+prelude
+public import Init.Data.Rat.Lemmas
+import Init.Data.Int.Bitwise.Lemmas
+import Init.Data.Int.DivMod.Lemmas
+
+/-!
+# The dyadic rationals
+
+Constructs the dyadic rationals as an ordered ring, equipped with a compatible embedding into the rationals.
+-/
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+open Nat
+
+namespace Int
+
+/-- The number of trailing zeros in the binary representation of `i`. -/
+def trailingZeros (i : Int) : Nat :=
+  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
+where
+  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
+    match k, (by omega : k ≠ 0) with
+    | k + 1, _ =>
+      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
+      else acc
+
+-- TODO: check performance of `trailingZeros` in the kernel and VM.
+
+private theorem trailingZeros_aux_irrel (hi : i ≠ 0) (hk : i.natAbs ≤ k) (hk' : i.natAbs ≤ k') :
+    trailingZeros.aux k i hi hk acc = trailingZeros.aux k' i hi hk' acc := by
+  fun_induction trailingZeros.aux k i hi hk acc generalizing k' <;>
+    fun_cases trailingZeros.aux k' _ _ hk' _
+  · rename_i ih _ _ _ _ _
+    exact ih _
+  · contradiction
+  · contradiction
+  · rfl
+
+private theorem trailingZeros_aux_succ :
+    trailingZeros.aux k i hi hk (acc + 1) = trailingZeros.aux k i hi hk acc + 1 := by
+  fun_induction trailingZeros.aux k i hi hk acc <;> simp_all [trailingZeros.aux]
+
+theorem trailingZeros_zero : trailingZeros 0 = 0 := rfl
+
+theorem trailingZeros_two_mul_add_one (i : Int) :
+    Int.trailingZeros (2 * i + 1) = 0 := by
+  unfold trailingZeros trailingZeros.aux
+  rw [dif_neg (by omega)]
+  split <;> simp_all
+
+theorem trailingZeros_eq_zero_of_mod_eq {i : Int} (h : i % 2 = 1) :
+    Int.trailingZeros i = 0 := by
+  unfold trailingZeros trailingZeros.aux
+  rw [dif_neg (by omega)]
+  split <;> simp_all
+
+theorem trailingZeros_two_mul {i : Int} (h : i ≠ 0) :
+    Int.trailingZeros (2 * i) = Int.trailingZeros i + 1 := by
+  rw [Int.trailingZeros, dif_neg (Int.mul_ne_zero (by decide) h), Int.trailingZeros.aux.eq_def]
+  simp only [ne_eq, mul_emod_right, ↓reduceDIte, Int.reduceEq, not_false_eq_true,
+    mul_ediv_cancel_left, Nat.zero_add]
+  split
+  rw [trailingZeros, trailingZeros_aux_succ, dif_neg h]
+  apply congrArg Nat.succ (trailingZeros_aux_irrel ..) <;> omega
+
+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]
+  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
+    rw [Int.zero_add, mul_ediv_cancel_left _ (by decide), trailingZeros_two_mul h, Nat.add_comm,
+      shiftRight_add, shiftRight_eq_div_pow _ 1]
+    simpa using shiftRight_trailingZeros_mod_two h
+  · rwa [Int.add_comm, trailingZeros_two_mul_add_one, shiftRight_zero]
+termination_by i.natAbs
+
+theorem two_pow_trailingZeros_dvd {i : Int} (h : i ≠ 0) :
+    2 ^ i.trailingZeros ∣ i := by
+  rcases i.emod_two_eq with h' | 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
+    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]
+    exact Int.one_dvd _
+termination_by i.natAbs
+
+theorem trailingZeros_shiftLeft {x : Int} (hx : x ≠ 0) (n : Nat) :
+    trailingZeros (x <<< n) = x.trailingZeros + n := by
+  have : NeZero x := ⟨hx⟩
+  induction n <;> simp [Int.shiftLeft_succ', trailingZeros_two_mul (NeZero.ne _), *, Nat.add_assoc]
+
+@[simp]
+theorem trailingZeros_neg (x : Int) : trailingZeros (-x) = x.trailingZeros := by
+  by_cases hx : x = 0
+  · simp [hx]
+  rcases x.emod_two_eq with h | h
+  · rcases Int.dvd_of_emod_eq_zero h with ⟨a, rfl⟩
+    simp only [Int.mul_ne_zero_iff, ne_eq, Int.reduceEq, not_false_eq_true, true_and] at hx
+    rw [← Int.mul_neg, trailingZeros_two_mul hx, trailingZeros_two_mul (Int.neg_ne_zero.mpr hx)]
+    rw [trailingZeros_neg]
+  · simp [trailingZeros_eq_zero_of_mod_eq, h]
+termination_by x.natAbs
+
+end Int
+
+/--
+A dyadic rational is either zero or of the form `n * 2^(-k)` for some (unique) `n k : Int`
+where `n` is odd.
+-/
+inductive Dyadic where
+  /-- The dyadic number `0`. -/
+  | zero
+  /-- The dyadic number `n * 2^(-k)` for some odd `n` and integer `k`. -/
+  | ofOdd (n : Int) (k : Int) (hn : n % 2 = 1)
+deriving DecidableEq
+
+namespace Dyadic
+
+/-- Returns the dyadic number representation of `i * 2 ^ (-exp)`. -/
+def ofIntWithPrec (i : Int) (prec : Int) : Dyadic :=
+  if h : i = 0 then .zero
+  else .ofOdd (i >>> i.trailingZeros) (prec - i.trailingZeros) (Int.shiftRight_trailingZeros_mod_two h)
+
+/-- Convert an integer to a dyadic number (which will necessarily have non-positive precision). -/
+def ofInt (i : Int) : Dyadic :=
+  Dyadic.ofIntWithPrec i 0
+
+instance (n : Nat) : OfNat Dyadic n where
+  ofNat := Dyadic.ofInt n
+
+instance : IntCast Dyadic := ⟨ofInt⟩
+instance : NatCast Dyadic := ⟨fun x => ofInt x⟩
+
+/-- Add two dyadic numbers. -/
+protected def add (x y : Dyadic) : Dyadic :=
+  match x, y with
+  | .zero, y => y
+  | x, .zero => x
+  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
+    match k₁ - k₂ with
+    | 0 => .ofIntWithPrec (n₁ + n₂) k₁
+    -- TODO: these `simp_all` calls where previously factored out into a `where finally` clause,
+    -- but there is apparently a bad interaction with the module system.
+    | (d@hd:(d' + 1) : Nat) => .ofOdd (n₁ + (n₂ <<< d)) k₁ (by simp_all [Int.shiftLeft_eq, Int.pow_succ, ← Int.mul_assoc])
+    | -(d + 1 : Nat) => .ofOdd (n₁ <<< (d + 1) + n₂) k₂ (by simp_all [Int.shiftLeft_eq, Int.pow_succ, ← Int.mul_assoc])
+
+instance : Add Dyadic := ⟨Dyadic.add⟩
+
+/-- Multiply two dyadic numbers. -/
+protected def mul (x y : Dyadic) : Dyadic :=
+  match x, y with
+  | .zero, _ => .zero
+  | _, .zero => .zero
+  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
+    .ofOdd (n₁ * n₂) (k₁ + k₂) (by rw [Int.mul_emod, hn₁, hn₂]; rfl)
+
+instance : Mul Dyadic := ⟨Dyadic.mul⟩
+
+/-- Multiply two dyadic numbers. -/
+protected def pow (x : Dyadic) (i : Nat) : Dyadic :=
+  match x with
+  | .zero => if i = 0 then 1 else 0
+  | .ofOdd n k hn =>
+    .ofOdd (n ^ i) (k * i) (by induction i <;> simp [Int.pow_succ, Int.mul_emod, *])
+
+instance : Pow Dyadic Nat := ⟨Dyadic.pow⟩
+
+/-- Negate a dyadic number. -/
+protected def neg (x : Dyadic) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | .ofOdd n k hn => .ofOdd (-n) k (by rwa [Int.neg_emod_two])
+
+instance : Neg Dyadic := ⟨Dyadic.neg⟩
+
+/-- Subtract two dyadic numbers. -/
+protected def sub (x y : Dyadic) : Dyadic := x + (- y)
+
+instance : Sub Dyadic := ⟨Dyadic.sub⟩
+
+/-- Shift a dyadic number left by `i` bits. -/
+protected def shiftLeft (x : Dyadic) (i : Int) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | .ofOdd n k hn => .ofOdd n (k - i) hn
+
+/-- Shift a dyadic number right by `i` bits. -/
+protected def shiftRight (x : Dyadic) (i : Int) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | .ofOdd n k hn => .ofOdd n (k + i) hn
+
+instance : HShiftLeft Dyadic Int Dyadic := ⟨Dyadic.shiftLeft⟩
+instance : HShiftRight Dyadic Int Dyadic := ⟨Dyadic.shiftRight⟩
+
+instance : HShiftLeft Dyadic Nat Dyadic := ⟨fun x y => x <<< (y : Int)⟩
+instance : HShiftRight Dyadic Nat Dyadic := ⟨fun x y => x >>> (y : Int)⟩
+
+-- TODO: move this
+theorem _root_.Int.natAbs_emod_two (i : Int) : i.natAbs % 2 = (i % 2).natAbs := by omega
+
+/-- Convert a dyadic number to a rational number. -/
+def toRat (x : Dyadic) : Rat :=
+  match x with
+  | .zero => 0
+  | .ofOdd n (k : Nat) hn =>
+    have reduced : n.natAbs.Coprime (2 ^ k) := by
+      apply Coprime.pow_right
+      rw [coprime_iff_gcd_eq_one, Nat.gcd_comm, Nat.gcd_def]
+      simp [hn, Int.natAbs_emod_two]
+    ⟨n, 2 ^ k, Nat.ne_of_gt (Nat.pow_pos (by decide)), reduced⟩
+  | .ofOdd n (-((k : Nat) + 1)) hn =>
+    (n * (2 ^ (k + 1) : Nat) : Int)
+
+@[simp] protected theorem zero_eq : Dyadic.zero = 0 := rfl
+@[simp] protected theorem add_zero (x : Dyadic) : x + 0 = x := by cases x <;> rfl
+@[simp] protected theorem zero_add (x : Dyadic) : 0 + x = x := by cases x <;> rfl
+@[simp] protected theorem neg_zero : (-0 : Dyadic) = 0 := rfl
+@[simp] protected theorem mul_zero (x : Dyadic) : x * 0 = 0 := by cases x <;> rfl
+@[simp] protected theorem zero_mul (x : Dyadic) : 0 * x = 0 := by cases x <;> rfl
+
+@[simp] theorem toRat_zero : toRat 0 = 0 := rfl
+
+theorem _root_.Rat.mkRat_one (x : Int) : mkRat x 1 = x := by
+  rw [← Rat.mk_den_one, Rat.mk_eq_mkRat]
+
+theorem toRat_ofOdd_eq_mkRat :
+    toRat (.ofOdd n k hn) = mkRat (n <<< (-k).toNat) (1 <<< k.toNat) := by
+  cases k
+  · simp [toRat, Rat.mk_eq_mkRat, Int.shiftLeft_eq, Nat.shiftLeft_eq]
+  · simp [toRat, Int.neg_negSucc, Rat.mkRat_one, Int.shiftLeft_eq]
+
+theorem toRat_ofIntWithPrec_eq_mkRat :
+    toRat (.ofIntWithPrec n k) = mkRat (n <<< (-k).toNat) (1 <<< k.toNat) := by
+  simp only [ofIntWithPrec]
+  split
+  · simp_all
+  rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
+  simp only [Int.natCast_shiftLeft, Int.cast_ofNat_Int, Int.shiftLeft_mul_shiftLeft, Int.mul_one]
+  have : (-(k - n.trailingZeros) : Int).toNat + k.toNat =
+      n.trailingZeros + ((-k).toNat + (k - n.trailingZeros).toNat) := by omega
+  rw [this, Int.shiftLeft_add, Int.shiftRight_shiftLeft_cancel]
+  exact Int.two_pow_trailingZeros_dvd ‹_›
+
+theorem toRat_ofIntWithPrec_eq_mul_two_pow : toRat (.ofIntWithPrec n k) = n * 2 ^ (-k) := by
+  rw [toRat_ofIntWithPrec_eq_mkRat, Rat.zpow_neg, Int.shiftLeft_eq, Nat.one_shiftLeft]
+  rw [Rat.mkRat_eq_div, Rat.div_def]
+  have : ((2 : Int) : Rat) ≠ 0 := by decide
+  simp only [Rat.intCast_mul, Rat.intCast_pow, ← Rat.zpow_natCast, ← Rat.intCast_natCast,
+    Int.natCast_pow, Int.cast_ofNat_Int, ← Rat.zpow_neg, Rat.mul_assoc, ne_eq,
+    Rat.intCast_eq_zero_iff, Int.reduceEq, not_false_eq_true, ← Rat.zpow_add]
+  rw [Int.add_neg_eq_sub, ← Int.neg_sub, Int.toNat_sub_toNat_neg]
+  rfl
+
+example : ((3 : Dyadic) >>> 2) + ((3 : Dyadic) >>> 2) = ((3 : Dyadic) >>> 1) := rfl -- 3/4 + 3/4 = 3/2
+example : ((7 : Dyadic) >>> 3) + ((1 : Dyadic) >>> 3) = 1 := rfl -- 7/8 + 1/8 = 1
+example : (12 : Dyadic) + ((3 : Dyadic) >>> 1) = (27 : Dyadic) >>> 1 := rfl -- 12 + 3/2 = 27/2 = (2 * 13 + 1)/2^1
+example : ((3 : Dyadic) >>> 1).add 12 =  (27 : Dyadic) >>> 1 := rfl -- 3/2 + 12 = 27/2 = (2 * 13 + 1)/2^1
+example : (12 : Dyadic).add 12 = 24 := rfl -- 12 + 12 = 24
+
+@[simp]
+theorem toRat_add (x y : Dyadic) : toRat (x + y) = toRat x + toRat y := by
+  match x, y with
+  | .zero, _ => simp [toRat, Rat.zero_add]
+  | _, .zero => simp [toRat, Rat.add_zero]
+  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
+    change (Dyadic.add _ _).toRat = _
+    rw [Dyadic.add, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat]
+    rw [Rat.mkRat_add_mkRat _ _ (NeZero.ne _) (NeZero.ne _)]
+    split
+    · rename_i h
+      cases Int.sub_eq_zero.mp h
+      rw [toRat_ofIntWithPrec_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
+      simp [Int.shiftLeft_mul_shiftLeft, Int.add_shiftLeft, Int.add_mul, Nat.add_assoc]
+    · rename_i h
+      cases Int.sub_eq_iff_eq_add.mp h
+      rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
+      simp only [succ_eq_add_one, Int.ofNat_eq_coe, Int.add_shiftLeft, ← Int.shiftLeft_add,
+        Int.natCast_mul, Int.natCast_shiftLeft, Int.shiftLeft_mul_shiftLeft, Int.add_mul]
+      congr 2 <;> omega
+    · rename_i h
+      cases Int.sub_eq_iff_eq_add.mp h
+      rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
+      simp only [Int.add_shiftLeft, ← Int.shiftLeft_add, Int.natCast_mul, Int.natCast_shiftLeft,
+        Int.cast_ofNat_Int, Int.shiftLeft_mul_shiftLeft, Int.mul_one, Int.add_mul]
+      congr 2 <;> omega
+
+@[simp]
+theorem toRat_neg (x : Dyadic) : toRat (-x) = - toRat x := by
+  change x.neg.toRat = _
+  cases x
+  · rfl
+  · simp [Dyadic.neg, Rat.neg_mkRat, Int.neg_shiftLeft, toRat_ofOdd_eq_mkRat]
+
+@[simp]
+theorem toRat_sub (x y : Dyadic) : toRat (x - y) = toRat x - toRat y := by
+  change toRat (x + -y) = _
+  simp [Rat.sub_eq_add_neg]
+
+@[simp]
+theorem toRat_mul (x y : Dyadic) : toRat (x * y) = toRat x * toRat y := by
+  match x, y with
+  | .zero, _ => simp
+  | _, .zero => simp
+  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
+    change (Dyadic.mul _ _).toRat = _
+    rw [Dyadic.mul, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat,
+      Rat.mkRat_mul_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
+    simp only [Int.natCast_mul, Int.natCast_shiftLeft, Int.cast_ofNat_Int,
+      Int.shiftLeft_mul_shiftLeft, Int.mul_one]
+    congr 1; omega
+
+@[simp]
+protected theorem pow_zero (x : Dyadic) : x ^ 0 = 1 := by
+  change x.pow 0 = 1
+  cases x <;> simp [Dyadic.pow] <;> rfl
+
+protected theorem pow_succ (x : Dyadic) (n : Nat) : x ^ (n + 1) = x ^ n * x := by
+  change x.pow (n + 1) = x.pow n * x
+  cases x
+  · simp [Dyadic.pow]
+  · change _ = Dyadic.mul _ _
+    simp [Dyadic.pow, Dyadic.mul, Int.pow_succ, Int.mul_add]
+
+@[simp]
+theorem toRat_pow (x : Dyadic) (n : Nat) : toRat (x ^ n) = toRat x ^ n := by
+  induction n with
+  | zero => simp; rfl
+  | succ k ih => simp [Dyadic.pow_succ, Rat.pow_succ, ih]
+
+@[simp]
+theorem toRat_intCast (x : Int) : (x : Dyadic).toRat = x := by
+  change (ofInt x).toRat = x
+  simp [ofInt, toRat_ofIntWithPrec_eq_mul_two_pow]
+
+@[simp]
+theorem toRat_natCast (x : Nat) : (x : Dyadic).toRat = x := by
+  change (ofInt x).toRat = x
+  simp [ofInt, toRat_ofIntWithPrec_eq_mul_two_pow, Rat.intCast_natCast]
+
+@[simp] theorem of_ne_zero : ofOdd n k hn ≠ 0 := Dyadic.noConfusion
+@[simp] theorem zero_ne_of : 0 ≠ ofOdd n k hn := Dyadic.noConfusion
+
+@[simp]
+theorem toRat_eq_zero_iff {x : Dyadic} : x.toRat = 0 ↔ x = 0 := by
+  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
+  cases x
+  · rfl
+  · simp only [toRat_ofOdd_eq_mkRat, ne_eq, shiftLeft_eq_zero_iff, succ_ne_self, not_false_eq_true,
+      Rat.mkRat_eq_zero, Int.shiftLeft_eq_zero_iff] at h
+    cases h
+    contradiction
+
+theorem ofOdd_eq_ofIntWithPrec : ofOdd n k hn = ofIntWithPrec n k := by
+  simp only [ofIntWithPrec, Dyadic.zero_eq, Int.trailingZeros_eq_zero_of_mod_eq hn,
+    Int.shiftRight_zero, Int.cast_ofNat_Int, Int.sub_zero, right_eq_dite_iff, of_ne_zero, imp_false]
+  intro rfl; contradiction
+
+theorem toRat_ofOdd_eq_mul_two_pow : toRat (.ofOdd n k hn) = n * 2 ^ (-k) := by
+  rw [ofOdd_eq_ofIntWithPrec, toRat_ofIntWithPrec_eq_mul_two_pow]
+
+@[simp]
+theorem ofIntWithPrec_zero {i : Int} : ofIntWithPrec 0 i = 0 := rfl
+
+@[simp]
+theorem neg_ofOdd : -ofOdd n k hn = ofOdd (-n) k (by simpa using hn) := rfl
+
+@[simp]
+theorem neg_ofIntWithPrec {i prec : Int} : -ofIntWithPrec i prec = ofIntWithPrec (-i) prec := by
+  rw [ofIntWithPrec, ofIntWithPrec]
+  simp only [Dyadic.zero_eq, Int.neg_eq_zero, Int.trailingZeros_neg]
+  split
+  · rfl
+  · obtain ⟨a, h⟩ := Int.two_pow_trailingZeros_dvd ‹_›
+    rw [Int.mul_comm, ← Int.shiftLeft_eq] at h
+    conv => enter [1, 1, 1, 1]; rw [h]
+    conv => enter [2, 1, 1]; rw [h]
+    simp only [Int.shiftLeft_shiftRight_cancel, neg_ofOdd, ← Int.neg_shiftLeft]
+
+theorem ofIntWithPrec_shiftLeft_add {n : Nat} :
+    ofIntWithPrec ((x : Int) <<< n) (i + n) = ofIntWithPrec x i := by
+  rw [ofIntWithPrec, ofIntWithPrec]
+  simp only [Int.shiftLeft_eq_zero_iff]
+  split
+  · rfl
+  · simp [Int.trailingZeros_shiftLeft, *, Int.shiftLeft_shiftRight_eq_shiftRight_of_le,
+      Int.add_comm x.trailingZeros n, ← Int.sub_sub]
+
+/-- The "precision" of a dyadic number, i.e. in `n * 2^(-p)` with `n` odd the precision is `p`. -/
+def precision : Dyadic → Int
+  | .zero => 0
+  | .ofOdd _ p _ => p
+
+/--
+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 :=
+  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) :
+    Rat.toDyadic (mkRat a b) prec =
+      .ofIntWithPrec ((a <<< prec.toNat) / (b <<< (-prec).toNat)) prec := by
+  by_cases hb : b = 0
+  · cases prec <;> simp [hb, Rat.toDyadic]
+  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,
+      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]
+    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv (by simp),
+      Int.mul_ediv_cancel _ (by simpa using hm)]
+
+/--
+Rounds a dyadic rational `x` down to the greatest dyadic number with precision at most `prec`
+which is less than or equal to `x`.
+-/
+def roundDown (x : Dyadic) (prec : Int) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | .ofOdd n k _ =>
+    match k - prec with
+    | .ofNat l => .ofIntWithPrec (n >>> l) prec
+    | .negSucc _ => x
+
+theorem roundDown_eq_self_of_le {x : Dyadic} {prec : Int} (h : x.precision ≤ prec) :
+    roundDown x prec = x := by
+  rcases x with _ | ⟨n, k, hn⟩
+  · rfl
+  · simp only [precision] at h
+    obtain ⟨a, rfl⟩ := h.dest
+    rcases a with _ | a
+    · simp [roundDown, ofOdd_eq_ofIntWithPrec]
+    · have : k - (k + (a + 1 : Nat)) = Int.negSucc a := by omega
+      simp only [roundDown, this]
+
+@[simp]
+theorem toDyadic_toRat (x : Dyadic) (prec : Int) :
+    x.toRat.toDyadic prec = x.roundDown prec := by
+  rcases x with _ | ⟨n, k, hn⟩
+  · cases prec <;> simp [Rat.toDyadic, roundDown]
+  · simp only [toRat_ofOdd_eq_mkRat, roundDown]
+    rw [Rat.toDyadic_mkRat]
+    simp only [← Int.shiftLeft_add, Int.natCast_shiftLeft, Int.cast_ofNat_Int]
+    rw [Int.shiftLeft_eq' 1, Int.one_mul, ← Int.shiftRight_eq_div_pow]
+    rw [Int.shiftLeft_shiftRight_eq, ← Int.toNat_sub, ← Int.toNat_sub, ← Int.neg_sub]
+    have : ((k.toNat + (-prec).toNat : Nat) - ((-k).toNat + prec.toNat : Nat) : Int) = k - prec := by
+      omega
+    rw [this]
+    cases h : k - prec
+    · simp
+    · simp
+      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]
+
+theorem toRat_inj {x y : Dyadic} : x.toRat = y.toRat ↔ x = y := by
+  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
+  cases x <;> cases y
+  · rfl
+  · simp [eq_comm (a := (0 : Rat))] at h
+  · simp at h
+  · rename_i n₁ k₁ hn₁ n₂ k₂ hn₂
+    replace h := congrArg (·.toDyadic (max k₁ k₂)) h
+    simpa [toDyadic_toRat, roundDown_eq_self_of_le, precision, Int.le_max_left, Int.le_max_right]
+      using h
+
+theorem add_comm (x y : Dyadic) : x + y = y + x := by
+  rw [← toRat_inj, toRat_add, toRat_add, Rat.add_comm]
+
+theorem add_assoc (x y z : Dyadic) : (x + y) + z = x + (y + z) := by
+  rw [← toRat_inj, toRat_add, toRat_add, toRat_add, toRat_add, Rat.add_assoc]
+
+theorem mul_comm (x y : Dyadic) : x * y = y * x := by
+  rw [← toRat_inj, toRat_mul, toRat_mul, Rat.mul_comm]
+
+theorem mul_assoc (x y z : Dyadic) : (x * y) * z = x * (y * z) := by
+  rw [← toRat_inj, toRat_mul, toRat_mul, toRat_mul, toRat_mul, Rat.mul_assoc]
+
+theorem mul_one (x : Dyadic) : x * 1 = x := by
+  rw [← toRat_inj, toRat_mul]
+  exact Rat.mul_one x.toRat
+
+theorem one_mul (x : Dyadic) : 1 * x = x := by
+  rw [← toRat_inj, toRat_mul]
+  exact Rat.one_mul x.toRat
+
+theorem add_mul (x y z : Dyadic) : (x + y) * z = x * z + y * z := by
+  simp [← toRat_inj, Rat.add_mul]
+
+theorem mul_add (x y z : Dyadic) : x * (y + z) = x * y + x * z := by
+  simp [← toRat_inj, Rat.mul_add]
+
+theorem neg_add_cancel (x : Dyadic) : -x + x = 0 := by
+  simp [← toRat_inj, Rat.neg_add_cancel]
+
+theorem neg_mul (x y : Dyadic) : -x * y = -(x * y) := by
+  simp [← toRat_inj, Rat.neg_mul]
+
+/-- Determine if a dyadic rational is strictly less than another. -/
+def blt (x y : Dyadic) : Bool :=
+  match x, y with
+  | .zero, .zero => false
+  | .zero, .ofOdd n₂ _ _ => 0 < n₂
+  | .ofOdd n₁ _ _, .zero => n₁ < 0
+  | .ofOdd n₁ k₁ _, .ofOdd n₂ k₂ _ =>
+    match k₂ - k₁ with
+    | (l : Nat) => (n₁ <<< l) < n₂
+    | -((l+1 : Nat)) => n₁ < (n₂ <<< (l + 1))
+
+/-- Determine if a dyadic rational is less than or equal to another. -/
+def ble (x y : Dyadic) : Bool :=
+  match x, y with
+  | .zero, .zero => true
+  | .zero, .ofOdd n₂ _ _ => 0 ≤ n₂
+  | .ofOdd n₁ _ _, .zero => n₁ ≤ 0
+  | .ofOdd n₁ k₁ _, .ofOdd n₂ k₂ _ =>
+    match k₂ - k₁ with
+    | (l : Nat) => (n₁ <<< l) ≤ n₂
+    | -((l+1 : Nat)) => n₁ ≤ (n₂ <<< (l + 1))
+
+theorem blt_iff_toRat {x y : Dyadic} : blt x y ↔ x.toRat < y.toRat := by
+  rcases x with _ | ⟨n₁, k₁, hn₁⟩ <;> rcases y with _ | ⟨n₂, k₂, hn₂⟩
+  · decide
+  · simp only [blt, decide_eq_true_eq, Dyadic.zero_eq, toRat_zero, toRat_ofOdd_eq_mul_two_pow,
+      Rat.mul_pos_iff_of_pos_right (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.intCast_pos]
+  · simp only [blt, decide_eq_true_eq, Dyadic.zero_eq, toRat_zero, toRat_ofOdd_eq_mul_two_pow,
+      Rat.mul_neg_iff_of_pos_right (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.intCast_neg_iff]
+  · simp only [blt, toRat_ofOdd_eq_mul_two_pow,
+      ← Rat.div_lt_iff (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.div_def, ← Rat.zpow_neg,
+      Int.neg_neg, Rat.mul_assoc, ne_eq, Rat.ofNat_eq_ofNat, reduceCtorEq, not_false_eq_true,
+      ← Rat.zpow_add, Int.shiftLeft_eq]
+    rw [Int.add_comm, Int.add_neg_eq_sub]
+    split
+    · simp [decide_eq_true_eq, ← Rat.intCast_lt_intCast, Rat.zpow_natCast, *]
+    · simp only [decide_eq_true_eq, Int.negSucc_eq, *]
+      rw [Rat.zpow_neg, ← Rat.div_def, Rat.div_lt_iff (Rat.zpow_pos (by decide))]
+      simp [← Rat.intCast_lt_intCast, ← Rat.zpow_natCast, *]
+
+theorem blt_eq_false_iff : blt x y = false ↔ ble y x = true := by
+  cases x <;> cases y
+  · simp [ble, blt]
+  · simp [ble, blt]
+  · simp [ble, blt]
+  · rename_i n₁ k₁ hn₁ n₂ k₂ hn₂
+    simp only [blt, ble]
+    rw [← Int.neg_sub]
+    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,
+        decide_eq_true_eq]
+
+theorem ble_iff_toRat : ble x y ↔ x.toRat ≤ y.toRat := by
+  rw [← blt_eq_false_iff, Bool.eq_false_iff]
+  simp only [ne_eq, blt_iff_toRat, Rat.not_lt]
+
+instance : LT Dyadic where
+  lt x y := blt x y
+
+instance : LE Dyadic where
+  le x y := ble x y
+
+instance : DecidableLT Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
+instance : DecidableLE Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
+
+theorem lt_iff_toRat {x y : Dyadic} : x < y ↔ x.toRat < y.toRat := blt_iff_toRat
+
+theorem le_iff_toRat {x y : Dyadic} : x ≤ y ↔ x.toRat ≤ y.toRat := ble_iff_toRat
+
+@[simp]
+protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by
+  simp only [· ≤ ·, · < ·, Bool.not_eq_true, blt_eq_false_iff]
+
+@[simp]
+protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by
+  rw [← Dyadic.not_le, Decidable.not_not]
+
+@[simp]
+protected theorem le_refl (x : Dyadic) : x ≤ x := by
+  rw [le_iff_toRat]
+  exact Rat.le_refl
+
+protected theorem le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := by
+  rw [le_iff_toRat] at h h' ⊢
+  exact Rat.le_trans h h'
+
+protected theorem le_antisymm {x y : Dyadic} (h : x ≤ y) (h' : y ≤ x) : x = y := by
+  rw [le_iff_toRat] at h h'
+  rw [← toRat_inj]
+  exact Rat.le_antisymm h h'
+
+protected theorem le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x := by
+  rw [le_iff_toRat, le_iff_toRat]
+  exact Rat.le_total
+
+instance : Std.LawfulOrderLT Dyadic where
+  lt_iff a b := by rw [← Dyadic.not_lt, iff_and_self]; exact (Dyadic.le_total _ _).resolve_left
+
+instance : Std.IsPreorder Dyadic where
+  le_refl := Dyadic.le_refl
+  le_trans _ _ _ := Dyadic.le_trans
+
+instance : Std.IsPartialOrder Dyadic where
+  le_antisymm _ _ := Dyadic.le_antisymm
+
+instance : Std.IsLinearPreorder Dyadic where
+  le_total := Dyadic.le_total
+
+instance : Std.IsLinearOrder Dyadic where
+
+end Dyadic

src/Init/Data/Dyadic/Instances.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Robin Arnez
+-/
+module
+
+prelude
+public import Init.Data.Dyadic.Basic
+public import Init.Grind.Ring.Basic
+public import Init.Grind.Ordered.Ring
+
+/-! # Internal `grind` algebra instances for `Dyadic`. -/
+
+open Lean.Grind
+
+namespace Dyadic
+
+instance : CommRing Dyadic where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
+  add_zero := Dyadic.add_zero
+  add_comm := Dyadic.add_comm
+  add_assoc := Dyadic.add_assoc
+  mul_assoc := Dyadic.mul_assoc
+  mul_one := Dyadic.mul_one
+  one_mul := Dyadic.one_mul
+  zero_mul := Dyadic.zero_mul
+  mul_zero := Dyadic.mul_zero
+  mul_comm := Dyadic.mul_comm
+  pow_zero := Dyadic.pow_zero
+  pow_succ := Dyadic.pow_succ
+  sub_eq_add_neg _ _ := rfl
+  neg_add_cancel := Dyadic.neg_add_cancel
+  neg_zsmul _ _ := by simp [← toRat_inj, Rat.neg_mul]
+  left_distrib := Dyadic.mul_add
+  right_distrib := Dyadic.add_mul
+  intCast_neg _ := by simp [← toRat_inj]
+  ofNat_succ n := by
+    change ((n + 1 : Int) : Dyadic) = ((n : Int) : Dyadic) + 1
+    simp [← toRat_inj, Rat.intCast_add]; rfl
+
+instance : IsCharP Dyadic 0 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by change (x : Dyadic) = 0 ↔ _; simp [← toRat_inj])
+
+instance : NoNatZeroDivisors Dyadic where
+  no_nat_zero_divisors k a b h₁ h₂ := by
+    change k * a = k * b at h₂
+    simp only [← toRat_inj, toRat_mul, toRat_natCast] at h₂ ⊢
+    simpa [← Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
+
+instance : LinearOrder Dyadic where
+  le_refl := Dyadic.le_refl
+  le_trans := Dyadic.le_trans
+  le_antisymm := Dyadic.le_antisymm
+  le_total := Dyadic.le_total
+  lt_iff_le_not_le := Std.LawfulOrderLT.lt_iff _ _
+
+instance : OrderedRing Dyadic where
+  zero_lt_one := by decide
+  add_le_left_iff _ := by simp [le_iff_toRat, Rat.add_le_add_right]
+  mul_lt_mul_of_pos_left {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_left
+  mul_lt_mul_of_pos_right {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_right
+
+end Dyadic

src/Init/Data/Rat/Lemmas.lean

@@ -251,8 +251,10 @@ theorem add_def (a b : Rat) :
 theorem add_def' (a b : Rat) : a + b = mkRat (a.num * b.den + b.num * a.den) (a.den * b.den) := by
   rw [add_def, normalize_eq_mkRat]
 
-@[simp] protected theorem add_zero (a : Rat) : a + 0 = a := by simp [add_def', mkRat_self]
-@[simp] protected theorem zero_add (a : Rat) : 0 + a = a := by simp [add_def', mkRat_self]
+@[local simp]
+protected theorem add_zero (a : Rat) : a + 0 = a := by simp [add_def', mkRat_self]
+@[local simp]
+protected theorem zero_add (a : Rat) : 0 + a = a := by simp [add_def', mkRat_self]
 
 theorem normalize_add_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
     normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ =
@@ -383,7 +385,7 @@ theorem mkRat_mul_mkRat (n₁ n₂ : Int) (d₁ d₂) :
   if z₁ : d₁ = 0 then simp [z₁] else if z₂ : d₂ = 0 then simp [z₂] else
   rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]
 
-theorem divInt_mul_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+theorem divInt_mul_divInt (n₁ n₂ : Int) {d₁ d₂} :
     (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂) := by
   rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
   rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
@@ -441,9 +443,22 @@ protected theorem mul_inv_cancel (a : Rat) : a ≠ 0 → a * a⁻¹ = 1 :=
 protected theorem inv_mul_cancel (a : Rat) (h : a ≠ 0) : a⁻¹ * a = 1 :=
   Eq.trans (Rat.mul_comm _ _) (Rat.mul_inv_cancel _ h)
 
+protected theorem inv_eq_of_mul_eq_one {a b : Rat} (h : a * b = 1) : a⁻¹ = b := by
+  have : a ≠ 0 := by intro h; simp_all +decide
+  simpa [← Rat.mul_assoc, Rat.inv_mul_cancel _ this, eq_comm] using congrArg (a⁻¹ * ·) h
+
 protected theorem inv_inv (a : Rat) : a⁻¹⁻¹ = a :=
   numDenCasesOn' a fun n d hd ↦ by simp only [inv_divInt]
 
+protected theorem inv_mul_rev (a b : Rat) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
+  by_cases ha : a = 0
+  · simp [ha]
+  by_cases hb : b = 0
+  · simp [hb]
+  apply Rat.inv_eq_of_mul_eq_one
+  rw [← Rat.mul_assoc, Rat.mul_assoc a, Rat.mul_inv_cancel _ hb, Rat.mul_one,
+    Rat.mul_inv_cancel _ ha]
+
 protected theorem mul_eq_zero {a b : Rat} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
   constructor
   · intro h
@@ -456,19 +471,34 @@ protected theorem mul_eq_zero {a b : Rat} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 
 theorem div_def (a b : Rat) : a / b = a * b⁻¹ := rfl
 
+theorem divInt_eq_div (a b : Int) : a /. b = a / b := by
+  rw [← Rat.mk_den_one, ← Rat.mk_den_one, Rat.mk'_eq_divInt, Rat.mk'_eq_divInt, div_def,
+    inv_divInt, divInt_mul_divInt, Int.cast_ofNat_Int, Int.mul_one, Int.one_mul]
+
+theorem mkRat_eq_div (a : Int) (b : Nat) : mkRat a b = a / b := by
+  rw [← divInt_ofNat, divInt_eq_div]; rfl
+
+protected theorem div_mul_cancel {a b : Rat} (hb : b ≠ 0) : a / b * b = a := by
+  rw [div_def, Rat.mul_assoc, Rat.inv_mul_cancel _ hb, Rat.mul_one]
+
+protected theorem mul_div_cancel {a b : Rat} (hb : b ≠ 0) : a * b / b = a := by
+  rw [div_def, Rat.mul_assoc, Rat.mul_inv_cancel _ hb, Rat.mul_one]
+
 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
 
-protected theorem pow_zero (q : Rat) : q ^ 0 = 1 := 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
   rcases q with ⟨n, d, hn, r⟩
   simp only [pow_def, Int.pow_succ, Nat.pow_succ]
-  simp only [mk'_eq_divInt, divInt_mul_divInt, Int.natCast_eq_zero, hn, Nat.pow_eq_zero,
-    not_false_eq_true, false_and, ne_eq, Int.natCast_mul]
+  simp only [mk'_eq_divInt, Int.natCast_mul, divInt_mul_divInt]
 
-protected theorem zpow_zero (q : Rat) : q ^ (0 : Int) = 1 := Rat.pow_zero q
+@[simp] protected theorem pow_one (q : Rat) : q ^ 1 = q := by simp [Rat.pow_succ]
+
+@[simp] protected theorem zpow_zero (q : Rat) : q ^ (0 : Int) = 1 := Rat.pow_zero q
+@[simp] protected theorem zpow_one (q : Rat) : q ^ (1 : Int) = q := Rat.pow_one q
 
 protected theorem zpow_natCast (q : Rat) (n : Nat) : q ^ (n : Int) = q ^ n := rfl
 
@@ -478,6 +508,30 @@ protected theorem zpow_neg (q : Rat) (n : Int) : q ^ (-n : Int) = (q ^ n)⁻¹ :
   · rfl
   · exact (Rat.inv_inv _).symm
 
+protected theorem zpow_add_one {q : Rat} (hq : q ≠ 0) (m : Int) :
+    q ^ (m + 1) = q ^ m * q := by
+  rcases m with _ | (_ | m)
+  · apply Rat.pow_succ
+  · simp [Rat.zpow_neg, Rat.inv_mul_cancel _ hq]
+  · change q ^ (-(m + 1 : Nat) : Int) = q ^ (-(m + 2 : Nat) : Int) * q
+    simp only [Rat.zpow_neg, Rat.zpow_natCast, Rat.pow_succ, Rat.inv_mul_rev]
+    rw [Rat.mul_comm (_ * _), ← Rat.mul_assoc, Rat.mul_inv_cancel _ hq, Rat.one_mul]
+
+protected theorem zpow_sub_one {q : Rat} (hq : q ≠ 0) (m : Int) :
+    q ^ (m - 1) = q ^ m * q⁻¹ := by
+  calc
+    _ = q ^ (m - 1) * q * q⁻¹ := by simp [Rat.mul_assoc, Rat.mul_inv_cancel _ hq]
+    _ = q ^ m * q⁻¹ := by simp [← Rat.zpow_add_one hq]
+
+protected theorem zpow_add {q : Rat} (hq : q ≠ 0) (m n : Int) :
+    q ^ (m + n) = q ^ m * q ^ n := by
+  rcases n with n | n
+  · induction n <;> simp_all [Rat.zpow_add_one hq, ← Int.add_assoc, Rat.mul_assoc]
+  · induction n with
+    | zero => simp [Rat.zpow_neg, ← Int.sub_eq_add_neg, Rat.zpow_sub_one hq]
+    | succ k ih => simp [← Int.negSucc_sub_one, ← Int.add_sub_assoc, Rat.zpow_sub_one hq, ih,
+      Rat.mul_assoc]
+
 /-! ### `ofScientific` -/
 
 theorem ofScientific_true_def : Rat.ofScientific m true e = mkRat m (10 ^ e) := by
@@ -496,43 +550,6 @@ theorem ofScientific_ofNat_ofNat :
     Rat.ofScientific (no_index (OfNat.ofNat m)) s (no_index (OfNat.ofNat e))
       = OfScientific.ofScientific m s e := rfl
 
-/-! ### `intCast` -/
-
-@[simp] theorem den_intCast (a : Int) : (a : Rat).den = 1 := rfl
-
-@[simp] theorem num_intCast (a : Int) : (a : Rat).num = a := rfl
-
-@[deprecated den_intCast (since := "2025-08-22")]
-abbrev intCast_den := @den_intCast
-@[deprecated num_intCast (since := "2025-08-22")]
-abbrev intCast_num := @num_intCast
-
-@[simp, norm_cast] theorem intCast_inj {a b : Int} : (a : Rat) = (b : Rat) ↔ a = b := by
-  constructor
-  · rintro ⟨⟩; rfl
-  · simp_all
-
-protected theorem intCast_zero : ((0 : Int) : Rat) = (0 : Rat) := rfl
-
-protected theorem intCast_one : ((1 : Int) : Rat) = (1 : Rat) := rfl
-
-@[simp, norm_cast] protected theorem intCast_add (a b : Int) :
-    ((a + b : Int) : Rat) = (a : Rat) + (b : Rat) := by
-  rw [add_def]
-  simp [normalize_eq]
-
-@[simp, norm_cast] protected theorem intCast_neg (a : Int) : ((-a : Int) : Rat) = -(a : Rat) := rfl
-
-@[simp, norm_cast] protected theorem intCast_sub (a b : Int) :
-    ((a - b : Int) : Rat) = (a : Rat) - (b : Rat) := by
-  rw [sub_def]
-  simp [normalize_eq]
-
-@[simp, norm_cast] protected theorem intCast_mul (a b : Int) :
-    ((a * b : Int) : Rat) = (a : Rat) * (b : Rat) := by
-  rw [mul_def]
-  simp [normalize_eq]
-
 /-! ### `≤` and `<` -/
 
 @[simp] theorem num_nonneg {q : Rat} : 0 ≤ q.num ↔ 0 ≤ q := by
@@ -579,8 +596,7 @@ protected theorem mul_nonneg {a b : Rat} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :
     numDenCasesOn' b fun n₂ d₂ h₂ => by
       have d₁0 : 0 < (d₁ : Int) := mod_cast Nat.pos_of_ne_zero h₁
       have d₂0 : 0 < (d₂ : Int) := mod_cast Nat.pos_of_ne_zero h₂
-      simp only [d₁0, d₂0, Int.mul_pos, divInt_nonneg_iff_of_pos_right,
-        divInt_mul_divInt _ _ (Int.ne_of_gt d₁0) (Int.ne_of_gt d₂0)]
+      simp only [d₁0, divInt_nonneg_iff_of_pos_right, d₂0, divInt_mul_divInt, Int.mul_pos]
       apply Int.mul_nonneg
 
 protected theorem not_le {a b : Rat} : ¬a ≤ b ↔ b < a := (Bool.not_eq_false _).to_iff
@@ -644,9 +660,13 @@ protected theorem le_antisymm {a b : Rat} (hab : a ≤ b) (hba : b ≤ a) : a =
 protected theorem le_of_lt {a b : Rat} (ha : a < b) : a ≤ b :=
   Rat.le_total.resolve_left (Rat.not_le.mpr ha)
 
+@[simp]
+protected theorem lt_irrefl {a : Rat} : ¬a < a :=
+  Rat.not_lt.mpr Rat.le_refl
+
 protected theorem ne_of_lt {a b : Rat} (ha : a < b) : a ≠ b := by
   intro rfl
-  exact Rat.not_le.mpr ha Rat.le_refl
+  exact Rat.lt_irrefl ha
 
 protected theorem ne_of_gt {a b : Rat} (ha : a < b) : b ≠ a :=
   (Rat.ne_of_lt ha).symm
@@ -662,6 +682,9 @@ protected theorem add_le_add_left {a b c : Rat} : c + a ≤ c + b ↔ a ≤ b :=
     Rat.add_zero, Rat.add_assoc, Rat.add_left_comm (-a), Rat.neg_add_cancel, Rat.add_zero,
     Rat.add_comm]
 
+protected theorem add_le_add_right {a b c : Rat} : a + c ≤ b + c ↔ a ≤ b := by
+  rw [Rat.add_comm _ c, Rat.add_comm _ c, Rat.add_le_add_left]
+
 protected theorem lt_iff_sub_pos (a b : Rat) : a < b ↔ 0 < b - a := by
   simp only [← Rat.not_le]
   apply not_congr
@@ -685,6 +708,209 @@ protected theorem mul_lt_mul_of_pos_left {a b c : Rat} (ha : a < b) (hc : 0 < c)
 
 protected theorem mul_lt_mul_of_pos_right {a b c : Rat} (ha : a < b) (hc : 0 < c) :
     a * c < b * c := by
-  rw [Rat.lt_iff_sub_pos, Rat.sub_eq_add_neg] at ha ⊢
-  rw [← Rat.neg_mul, ← Rat.add_mul]
-  exact Rat.mul_pos ha hc
+  rw [Rat.mul_comm _ c, Rat.mul_comm _ c]
+  exact Rat.mul_lt_mul_of_pos_left ha hc
+
+protected theorem le_of_mul_le_mul_left {a b c : Rat} (ha : c * a ≤ c * b) (hc : 0 < c) :
+    a ≤ b := by
+  simp only [← Rat.not_lt] at ha ⊢
+  exact mt (Rat.mul_lt_mul_of_pos_left · hc) ha
+
+protected theorem le_of_mul_le_mul_right {a b c : Rat} (ha : a * c ≤ b * c) (hc : 0 < c) :
+    a ≤ b := by
+  rw [Rat.mul_comm _ c, Rat.mul_comm _ c] at ha
+  exact Rat.le_of_mul_le_mul_left ha hc
+
+protected theorem lt_of_mul_lt_mul_left {a b c : Rat} (h : c * a < c * b) (hc : 0 ≤ c) :
+    a < b := by
+  have hc' : 0 ≠ c := by intro rfl; simp at h
+  apply Rat.lt_of_le_of_ne
+  · exact Rat.le_of_mul_le_mul_left (Rat.le_of_lt h) (Rat.lt_of_le_of_ne hc hc')
+  · intro rfl
+    exact Rat.lt_irrefl h
+
+protected theorem lt_of_mul_lt_mul_right {a b c : Rat} (h : a * c < b * c) (hc : 0 ≤ c) :
+    a < b := by
+  rw [Rat.mul_comm _ c, Rat.mul_comm _ c] at h
+  exact Rat.lt_of_mul_lt_mul_left h hc
+
+protected theorem mul_lt_mul_left {a b c : Rat} (hc : 0 < c) : c * a < c * b ↔ a < b :=
+  ⟨(Rat.lt_of_mul_lt_mul_left · (Rat.le_of_lt hc)), (Rat.mul_lt_mul_of_pos_left · hc)⟩
+
+protected theorem mul_lt_mul_right {a b c : Rat} (hc : 0 < c) : a * c < b * c ↔ a < b :=
+  ⟨(Rat.lt_of_mul_lt_mul_right · (Rat.le_of_lt hc)), (Rat.mul_lt_mul_of_pos_right · hc)⟩
+
+protected theorem mul_pos_iff_of_pos_left {a b : Rat} (ha : 0 < a) : 0 < a * b ↔ 0 < b := by
+  constructor
+  · intro h
+    rw [← Rat.mul_zero a] at h
+    exact Rat.lt_of_mul_lt_mul_left h (Rat.le_of_lt ha)
+  · exact Rat.mul_pos ha
+
+protected theorem mul_pos_iff_of_pos_right {a b : Rat} (hb : 0 < b) : 0 < a * b ↔ 0 < a := by
+  rw [Rat.mul_comm, Rat.mul_pos_iff_of_pos_left hb]
+
+protected theorem mul_neg_iff_of_pos_left {a b : Rat} (ha : 0 < a) : a * b < 0 ↔ b < 0 := by
+  constructor
+  · intro h
+    rw [← Rat.mul_zero a] at h
+    exact Rat.lt_of_mul_lt_mul_left h (Rat.le_of_lt ha)
+  · intro h
+    simpa using Rat.mul_lt_mul_of_pos_left h ha
+
+protected theorem mul_neg_iff_of_pos_right {a b : Rat} (hb : 0 < b) : a * b < 0 ↔ a < 0 := by
+  rw [Rat.mul_comm, Rat.mul_neg_iff_of_pos_left hb]
+
+protected theorem inv_pos {a : Rat} : 0 < a⁻¹ ↔ 0 < a := by
+  suffices ∀ a : Rat, 0 < a → 0 < a⁻¹ from ⟨fun h => Rat.inv_inv a ▸ this _ h, this a⟩
+  intro a ha
+  apply Rat.lt_of_mul_lt_mul_left _ (Rat.le_of_lt ha)
+  apply Rat.lt_of_mul_lt_mul_left _ (Rat.le_of_lt ha)
+  simpa [Rat.mul_inv_cancel _ (Rat.ne_of_gt ha)]
+
+protected theorem pow_pos {a : Rat} {n : Nat} (h : 0 < a) : 0 < a ^ n := by
+  induction n with
+  | zero => simp +decide
+  | succ k ih => rw [Rat.pow_succ]; exact Rat.mul_pos ih h
+
+protected theorem zpow_pos {a : Rat} {n : Int} (h : 0 < a) : 0 < a ^ n := by
+  cases n
+  · simp [Rat.zpow_natCast, Rat.pow_pos h]
+  · simp only [Int.negSucc_eq, Rat.zpow_neg, Rat.inv_pos, ← Int.natCast_add_one,
+      Rat.zpow_natCast, Rat.pow_pos h]
+
+protected theorem div_lt_iff {a b c : Rat} (hb : 0 < b) : a / b < c ↔ a < c * b := by
+  rw [← Rat.mul_lt_mul_right hb, Rat.div_mul_cancel (Rat.ne_of_gt hb)]
+
+protected theorem div_lt_iff' {a b c : Rat} (hb : 0 < b) : a / b < c ↔ a < b * c := by
+  rw [Rat.div_lt_iff hb, Rat.mul_comm]
+
+protected theorem lt_div_iff {a b c : Rat} (hc : 0 < c) : a < b / c ↔ a * c < b := by
+  rw [← Rat.mul_lt_mul_right hc, Rat.div_mul_cancel (Rat.ne_of_gt hc)]
+
+protected theorem lt_div_iff' {a b c : Rat} (hc : 0 < c) : a < b / c ↔ c * a < b := by
+  rw [Rat.lt_div_iff hc, Rat.mul_comm]
+
+/-! ### `intCast` -/
+
+@[simp] theorem den_intCast (a : Int) : (a : Rat).den = 1 := rfl
+
+@[simp] theorem num_intCast (a : Int) : (a : Rat).num = a := rfl
+
+@[deprecated den_intCast (since := "2025-08-22")]
+abbrev intCast_den := @den_intCast
+@[deprecated num_intCast (since := "2025-08-22")]
+abbrev intCast_num := @num_intCast
+
+/-!
+The following lemmas are later subsumed by e.g. `Int.cast_add` and `Int.cast_mul` in Mathlib
+but it is convenient to have these earlier, for users who only need `Int` and `Rat`.
+-/
+
+@[norm_cast] theorem intCast_natCast (n : Nat) : ((n : Int) : Rat) = n := rfl
+
+@[simp, norm_cast] theorem intCast_inj {a b : Int} : (a : Rat) = (b : Rat) ↔ a = b := by
+  constructor
+  · rintro ⟨⟩; rfl
+  · simp_all
+
+@[simp, norm_cast] theorem natCast_inj {a b : Nat} : (a : Rat) = (b : Rat) ↔ a = b := by
+  constructor
+  · rintro ⟨⟩; rfl
+  · simp_all
+
+@[simp, norm_cast] theorem intCast_eq_zero_iff {a : Int} : (a : Rat) = 0 ↔ a = 0 :=
+  intCast_inj
+
+@[simp, norm_cast] theorem natCast_eq_zero_iff {a : Nat} : (a : Rat) = 0 ↔ a = 0 :=
+  natCast_inj
+
+@[simp] theorem ofNat_eq_ofNat {a b : Nat} :
+    no_index (OfNat.ofNat a : Rat) = no_index (OfNat.ofNat b : Rat) ↔ a = b :=
+  natCast_inj
+
+@[simp, norm_cast] theorem intCast_ofNat {a : Nat} :
+    (no_index (OfNat.ofNat a : Int) : Rat) = OfNat.ofNat a :=
+  rfl
+
+@[simp, norm_cast] theorem natCast_ofNat {a : Nat} :
+    (no_index (OfNat.ofNat a : Nat) : Rat) = OfNat.ofNat a :=
+  rfl
+
+protected theorem intCast_zero : ((0 : Int) : Rat) = (0 : Rat) := rfl
+
+protected theorem intCast_one : ((1 : Int) : Rat) = (1 : Rat) := rfl
+
+@[simp, norm_cast] protected theorem intCast_add (a b : Int) :
+    ((a + b : Int) : Rat) = (a : Rat) + (b : Rat) := by
+  rw [add_def]
+  simp [normalize_eq]
+
+@[simp, norm_cast] theorem natCast_add (a b : Nat) :
+    ((a + b : Nat) : Rat) = (a : Rat) + (b : Rat) := by
+  simp [← intCast_natCast]
+
+@[simp, norm_cast] protected theorem intCast_neg (a : Int) : ((-a : Int) : Rat) = -(a : Rat) := rfl
+
+@[simp, norm_cast] protected theorem intCast_sub (a b : Int) :
+    ((a - b : Int) : Rat) = (a : Rat) - (b : Rat) := by
+  rw [sub_def]
+  simp [normalize_eq]
+
+@[simp, norm_cast] protected theorem intCast_mul (a b : Int) :
+    ((a * b : Int) : Rat) = (a : Rat) * (b : Rat) := by
+  rw [mul_def]
+  simp [normalize_eq]
+
+@[simp, norm_cast] theorem natCast_mul (a b : Nat) :
+    ((a * b : Nat) : Rat) = (a : Rat) * (b : Rat) := by
+  simp [← intCast_natCast]
+
+@[simp, norm_cast] theorem intCast_pow (a : Int) (n : Nat) :
+    ((a ^ n : Int) : Rat) = (a : Rat) ^ n := by
+  simp [pow_def]
+
+@[simp, norm_cast] theorem natCast_pow (a b : Nat) :
+    ((a ^ b : Nat) : Rat) = (a : Rat) ^ b := by
+  simp [← intCast_natCast]
+
+@[norm_cast]
+theorem intCast_le_intCast {a b : Int} :
+    (a : Rat) ≤ (b : Rat) ↔ a ≤ b := by
+  simp [Rat.le_iff]
+
+@[norm_cast]
+theorem intCast_lt_intCast {a b : Int} :
+    (a : Rat) < (b : Rat) ↔ a < b := by
+  simp [Rat.lt_iff]
+
+@[norm_cast]
+theorem natCast_le_natCast {a b : Nat} :
+    (a : Rat) ≤ (b : Rat) ↔ a ≤ b := by
+  simp [← intCast_natCast, intCast_le_intCast]
+
+@[norm_cast]
+theorem natCast_lt_natCast {a b : Nat} :
+    (a : Rat) < (b : Rat) ↔ a < b := by
+  simp [← intCast_natCast, intCast_lt_intCast]
+
+theorem intCast_nonneg {a : Int} :
+    0 ≤ (a : Rat) ↔ 0 ≤ a :=
+  Rat.intCast_le_intCast
+
+theorem natCast_nonneg {a : Nat} : 0 ≤ (a : Rat) :=
+  Rat.intCast_nonneg.mpr (Int.natCast_nonneg _)
+
+theorem intCast_pos {a : Int} : 0 < (a : Rat) ↔ 0 < a :=
+  Rat.intCast_lt_intCast
+
+theorem natCast_pos {a : Nat} : 0 < (a : Rat) ↔ 0 < a :=
+  intCast_pos.trans Int.natCast_pos
+
+theorem intCast_nonpos {a : Int} :
+    (a : Rat) ≤ 0 ↔ a ≤ 0 :=
+  Rat.intCast_le_intCast
+
+theorem intCast_neg_iff {a : Int} :
+    (a : Rat) < 0 ↔ a < 0 :=
+  Rat.intCast_lt_intCast

src/Init/GrindInstances/Ring/Rat.lean

@@ -51,8 +51,7 @@ instance : IsCharP Rat 0 := IsCharP.mk' _ _
 
 instance : NoNatZeroDivisors Rat where
   no_nat_zero_divisors k a b h₁ h₂ := by
-    replace h₁ : (k : Rat) ≠ 0 := by change ((k : Int) : Rat) ≠ ((0 : Int) : Rat); simp [h₁]
-    replace h₂ : (k : Rat)⁻¹ * (k * a) = (k : Rat)⁻¹ * (k * b) := congrArg (_ * ·) h₂
-    simpa only [← Rat.mul_assoc, Rat.inv_mul_cancel _ h₁, Rat.one_mul] using h₂
+    change k * a = k * b at h₂
+    simpa [← Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
 
 end Lean.Grind