fix tests; just use the new Rat instead of the internal one, which we'll remove soon

src/Init/Data.lean

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

src/Init/Data/Nat.lean

@@ -10,6 +10,7 @@ public import Init.Data.Nat.Basic
 public import Init.Data.Nat.Div
 public import Init.Data.Nat.Dvd
 public import Init.Data.Nat.Gcd
+public import Init.Data.Nat.Coprime
 public import Init.Data.Nat.MinMax
 public import Init.Data.Nat.Order
 public import Init.Data.Nat.Bitwise

src/Init/Data/Nat/Coprime.lean

@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+module
+prelude
+
+public import Init.Data.Nat.Gcd
+
+public section
+
+/-!
+# Definitions and properties of `coprime`
+-/
+
+namespace Nat
+
+/-!
+### `coprime`
+-/
+
+/-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/
+@[reducible, expose] def Coprime (m n : Nat) : Prop := gcd m n = 1
+
+-- if we don't inline this, then the compiler computes the GCD even if it already has it
+@[inline] instance (m n : Nat) : Decidable (Coprime m n) := inferInstanceAs (Decidable (_ = 1))
+
+theorem coprime_iff_gcd_eq_one : Coprime m n ↔ gcd m n = 1 := .rfl
+
+theorem Coprime.gcd_eq_one : Coprime m n → gcd m n = 1 := id
+
+theorem Coprime.symm : Coprime n m → Coprime m n := (gcd_comm m n).trans
+
+theorem coprime_comm : Coprime n m ↔ Coprime m n := ⟨Coprime.symm, Coprime.symm⟩
+
+theorem Coprime.dvd_of_dvd_mul_right (H1 : Coprime k n) (H2 : k ∣ m * n) : k ∣ m := by
+  have t := dvd_gcd (Nat.dvd_mul_left k m) H2
+  rwa [gcd_mul_left, H1.gcd_eq_one, Nat.mul_one] at t
+
+theorem Coprime.dvd_of_dvd_mul_left (H1 : Coprime k m) (H2 : k ∣ m * n) : k ∣ n :=
+  H1.dvd_of_dvd_mul_right (by rwa [Nat.mul_comm])
+
+theorem Coprime.gcd_mul_left_cancel (m : Nat) (H : Coprime k n) : gcd (k * m) n = gcd m n :=
+  have H1 : Coprime (gcd (k * m) n) k := by
+    rw [Coprime, Nat.gcd_assoc, H.symm.gcd_eq_one, gcd_one_right]
+  Nat.dvd_antisymm
+    (dvd_gcd (H1.dvd_of_dvd_mul_left (gcd_dvd_left _ _)) (gcd_dvd_right _ _))
+    (gcd_dvd_gcd_mul_left_left _ _ _)
+
+theorem Coprime.gcd_mul_right_cancel (m : Nat) (H : Coprime k n) : gcd (m * k) n = gcd m n := by
+  rw [Nat.mul_comm m k, H.gcd_mul_left_cancel m]
+
+theorem Coprime.gcd_mul_left_cancel_right (n : Nat)
+    (H : Coprime k m) : gcd m (k * n) = gcd m n := by
+  rw [gcd_comm m n, gcd_comm m (k * n), H.gcd_mul_left_cancel n]
+
+theorem Coprime.gcd_mul_right_cancel_right (n : Nat)
+    (H : Coprime k m) : gcd m (n * k) = gcd m n := by
+  rw [Nat.mul_comm n k, H.gcd_mul_left_cancel_right n]
+
+theorem coprime_div_gcd_div_gcd
+    (H : 0 < gcd m n) : Coprime (m / gcd m n) (n / gcd m n) := by
+  rw [coprime_iff_gcd_eq_one, gcd_div (gcd_dvd_left m n) (gcd_dvd_right m n), Nat.div_self H]
+
+theorem not_coprime_of_dvd_of_dvd (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) : ¬ Coprime m n :=
+  fun co => Nat.not_le_of_gt dgt1 <| Nat.le_of_dvd Nat.zero_lt_one <| by
+    rw [← co.gcd_eq_one]; exact dvd_gcd Hm Hn
+
+theorem exists_coprime (m n : Nat) :
+    ∃ m' n', Coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n := by
+  cases eq_zero_or_pos (gcd m n) with
+  | inl h0 =>
+    rw [gcd_eq_zero_iff] at h0
+    refine ⟨1, 1, gcd_one_left 1, ?_⟩
+    simp [h0]
+  | inr hpos =>
+    exact ⟨_, _, coprime_div_gcd_div_gcd hpos,
+      (Nat.div_mul_cancel (gcd_dvd_left m n)).symm,
+      (Nat.div_mul_cancel (gcd_dvd_right m n)).symm⟩
+
+theorem exists_coprime' (H : 0 < gcd m n) :
+    ∃ g m' n', 0 < g ∧ Coprime m' n' ∧ m = m' * g ∧ n = n' * g :=
+  let ⟨m', n', h⟩ := exists_coprime m n; ⟨_, m', n', H, h⟩
+
+theorem Coprime.mul_left (H1 : Coprime m k) (H2 : Coprime n k) : Coprime (m * n) k :=
+  (H1.gcd_mul_left_cancel n).trans H2
+
+theorem Coprime.mul_right (H1 : Coprime k m) (H2 : Coprime k n) : Coprime k (m * n) :=
+  (H1.symm.mul_left H2.symm).symm
+
+theorem Coprime.coprime_dvd_left (H1 : m ∣ k) (H2 : Coprime k n) : Coprime m n := by
+  apply eq_one_of_dvd_one
+  rw [Coprime] at H2
+  have := Nat.gcd_dvd_gcd_of_dvd_left n H1
+  rwa [← H2]
+
+theorem Coprime.coprime_dvd_right (H1 : n ∣ m) (H2 : Coprime k m) : Coprime k n :=
+  (H2.symm.coprime_dvd_left H1).symm
+
+theorem Coprime.coprime_mul_left (H : Coprime (k * m) n) : Coprime m n :=
+  H.coprime_dvd_left (Nat.dvd_mul_left _ _)
+
+theorem Coprime.coprime_mul_right (H : Coprime (m * k) n) : Coprime m n :=
+  H.coprime_dvd_left (Nat.dvd_mul_right _ _)
+
+theorem Coprime.coprime_mul_left_right (H : Coprime m (k * n)) : Coprime m n :=
+  H.coprime_dvd_right (Nat.dvd_mul_left _ _)
+
+theorem Coprime.coprime_mul_right_right (H : Coprime m (n * k)) : Coprime m n :=
+  H.coprime_dvd_right (Nat.dvd_mul_right _ _)
+
+theorem Coprime.coprime_div_left (cmn : Coprime m n) (dvd : a ∣ m) : Coprime (m / a) n := by
+  match eq_zero_or_pos a with
+  | .inl h0 =>
+    rw [h0] at dvd
+    rw [Nat.eq_zero_of_zero_dvd dvd] at cmn ⊢
+    simp; assumption
+  | .inr hpos =>
+    let ⟨k, hk⟩ := dvd
+    rw [hk, Nat.mul_div_cancel_left _ hpos]
+    rw [hk] at cmn
+    exact cmn.coprime_mul_left
+
+theorem Coprime.coprime_div_right (cmn : Coprime m n) (dvd : a ∣ n) : Coprime m (n / a) :=
+  (cmn.symm.coprime_div_left dvd).symm
+
+theorem coprime_mul_iff_left : Coprime (m * n) k ↔ Coprime m k ∧ Coprime n k :=
+  ⟨fun h => ⟨h.coprime_mul_right, h.coprime_mul_left⟩,
+   fun ⟨h, _⟩ => by rwa [coprime_iff_gcd_eq_one, h.gcd_mul_left_cancel n]⟩
+
+theorem coprime_mul_iff_right : Coprime k (m * n) ↔ Coprime k m ∧ Coprime k n := by
+  rw [@coprime_comm k, @coprime_comm k, @coprime_comm k, coprime_mul_iff_left]
+
+theorem Coprime.gcd_left (k : Nat) (hmn : Coprime m n) : Coprime (gcd k m) n :=
+  hmn.coprime_dvd_left <| gcd_dvd_right k m
+
+theorem Coprime.gcd_right (k : Nat) (hmn : Coprime m n) : Coprime m (gcd k n) :=
+  hmn.coprime_dvd_right <| gcd_dvd_right k n
+
+theorem Coprime.gcd_both (k l : Nat) (hmn : Coprime m n) : Coprime (gcd k m) (gcd l n) :=
+  (hmn.gcd_left k).gcd_right l
+
+theorem Coprime.mul_dvd_of_dvd_of_dvd (hmn : Coprime m n) (hm : m ∣ a) (hn : n ∣ a) : m * n ∣ a :=
+  let ⟨_, hk⟩ := hm
+  hk.symm ▸ Nat.mul_dvd_mul_left _ (hmn.symm.dvd_of_dvd_mul_left (hk ▸ hn))
+
+@[simp] theorem coprime_zero_left (n : Nat) : Coprime 0 n ↔ n = 1 := by simp [Coprime]
+
+@[simp] theorem coprime_zero_right (n : Nat) : Coprime n 0 ↔ n = 1 := by simp [Coprime]
+
+theorem coprime_one_left : ∀ n, Coprime 1 n := gcd_one_left
+
+theorem coprime_one_right : ∀ n, Coprime n 1 := gcd_one_right
+
+@[simp] theorem coprime_one_left_eq_true (n) : Coprime 1 n = True := eq_true (coprime_one_left _)
+
+@[simp] theorem coprime_one_right_eq_true (n) : Coprime n 1 = True := eq_true (coprime_one_right _)
+
+@[simp] theorem coprime_self (n : Nat) : Coprime n n ↔ n = 1 := by simp [Coprime]
+
+theorem Coprime.pow_left (n : Nat) (H1 : Coprime m k) : Coprime (m ^ n) k := by
+  induction n with
+  | zero => exact coprime_one_left _
+  | succ n ih => have hm := H1.mul_left ih; rwa [Nat.pow_succ, Nat.mul_comm]
+
+theorem Coprime.pow_right (n : Nat) (H1 : Coprime k m) : Coprime k (m ^ n) :=
+  (H1.symm.pow_left n).symm
+
+theorem Coprime.pow {k l : Nat} (m n : Nat) (H1 : Coprime k l) : Coprime (k ^ m) (l ^ n) :=
+  (H1.pow_left _).pow_right _
+
+theorem Coprime.eq_one_of_dvd {k m : Nat} (H : Coprime k m) (d : k ∣ m) : k = 1 := by
+  rw [← H.gcd_eq_one, gcd_eq_left d]
+
+theorem Coprime.gcd_mul (k : Nat) (h : Coprime m n) : gcd k (m * n) = gcd k m * gcd k n :=
+  Nat.dvd_antisymm
+    (gcd_mul_right_dvd_mul_gcd k m n)
+    ((h.gcd_both k k).mul_dvd_of_dvd_of_dvd
+      (gcd_dvd_gcd_mul_right_right ..)
+      (gcd_dvd_gcd_mul_left_right ..))
+
+theorem Coprime.mul_gcd (h : Coprime m n) (k : Nat) : gcd (m * n) k = gcd m k * gcd n k := by
+  rw [gcd_comm, h.gcd_mul, gcd_comm k, gcd_comm k]
+
+theorem gcd_mul_gcd_of_coprime_of_mul_eq_mul
+    (cop : Coprime c d) (h : a * b = c * d) : a.gcd c * b.gcd c = c := by
+  apply Nat.dvd_antisymm
+  · apply ((cop.gcd_left _).mul_left (cop.gcd_left _)).dvd_of_dvd_mul_right
+    rw [← h]
+    apply Nat.mul_dvd_mul (gcd_dvd ..).1 (gcd_dvd ..).1
+  · rw [gcd_comm a, gcd_comm b]
+    refine Nat.dvd_trans ?_ (gcd_mul_right_dvd_mul_gcd ..)
+    rw [h, gcd_mul_right_right d c]; apply Nat.dvd_refl

src/Init/Data/Rat.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.Rat.Basic
+public import Init.Data.Rat.Lemmas

src/Init/Data/Rat/Basic.lean

@@ -0,0 +1,295 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+module
+
+prelude
+public import Init.Data.Nat.Coprime
+public import Init.Data.Hashable
+public import Init.Data.OfScientific
+
+@[expose] public section
+
+/-! # Basics for the Rational Numbers -/
+
+/--
+Rational numbers, implemented as a pair of integers `num / den` such that the
+denominator is positive and the numerator and denominator are coprime.
+-/
+-- `Rat` is not tagged with the `ext` attribute, since this is more often than not undesirable
+structure Rat where
+  /-- Constructs a rational number from components.
+  We rename the constructor to `mk'` to avoid a clash with the smart constructor. -/
+  mk' ::
+  /-- The numerator of the rational number is an integer. -/
+  num : Int
+  /-- The denominator of the rational number is a natural number. -/
+  den : Nat := 1
+  /-- The denominator is nonzero. -/
+  den_nz : den ≠ 0 := by decide
+  /-- The numerator and denominator are coprime: it is in "reduced form". -/
+  reduced : num.natAbs.Coprime den := by decide
+  deriving DecidableEq, Hashable
+
+instance : Inhabited Rat := ⟨{ num := 0 }⟩
+
+instance : ToString Rat where
+  toString a := if a.den = 1 then toString a.num else s!"{a.num}/{a.den}"
+
+instance : Repr Rat where
+  reprPrec a _ := if a.den = 1 then repr a.num else s!"({a.num} : Rat)/{a.den}"
+
+theorem Rat.den_pos (self : Rat) : 0 < self.den := Nat.pos_of_ne_zero self.den_nz
+
+/--
+Auxiliary definition for `Rat.normalize`. Constructs `num / den` as a rational number,
+dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not 1.
+-/
+@[inline] def Rat.maybeNormalize (num : Int) (den g : Nat)
+    (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0)
+    (reduced : (num / g).natAbs.Coprime (den / g)) : Rat :=
+  if hg : g = 1 then
+    { num, den
+      den_nz := by simp [hg] at den_nz; exact den_nz
+      reduced := by simp [hg] at reduced; exact reduced }
+  else { num := num.divExact g dvd_num, den := den.divExact g dvd_den, den_nz, reduced }
+
+theorem Rat.normalize.dvd_num {num : Int} {den g : Nat}
+    (e : g = num.natAbs.gcd den) : ↑g ∣ num := by
+  rw [e, ← Int.dvd_natAbs, Int.ofNat_dvd]
+  exact Nat.gcd_dvd_left num.natAbs den
+
+theorem Rat.normalize.dvd_den {num : Int} {den g : Nat}
+    (e : g = num.natAbs.gcd den) : g ∣ den :=
+  e ▸ Nat.gcd_dvd_right ..
+
+theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0)
+    (e : g = num.natAbs.gcd den) : den / g ≠ 0 :=
+  e ▸ Nat.ne_of_gt (Nat.div_gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
+
+theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0)
+    (e : g = num.natAbs.gcd den) : (num / g).natAbs.Coprime (den / g) :=
+  have : Int.natAbs (num / ↑g) = num.natAbs / g := by
+    rw [Int.natAbs_ediv_of_dvd (dvd_num e), Int.natAbs_natCast]
+  this ▸ e ▸ Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
+
+/--
+Construct a normalized `Rat` from a numerator and nonzero denominator.
+This is a "smart constructor" that divides the numerator and denominator by
+the gcd to ensure that the resulting rational number is normalized.
+-/
+@[inline] def Rat.normalize (num : Int) (den : Nat := 1) (den_nz : den ≠ 0 := by decide) : Rat :=
+  Rat.maybeNormalize num den (num.natAbs.gcd den)
+    (normalize.dvd_num rfl) (normalize.dvd_den rfl)
+    (normalize.den_nz den_nz rfl) (normalize.reduced den_nz rfl)
+
+/--
+Construct a rational number from a numerator and denominator.
+This is a "smart constructor" that divides the numerator and denominator by
+the gcd to ensure that the resulting rational number is normalized, and returns
+zero if `den` is zero.
+-/
+def mkRat (num : Int) (den : Nat) : Rat :=
+  if den_nz : den = 0 then { num := 0 } else Rat.normalize num den den_nz
+
+namespace Rat
+
+/-- Embedding of `Int` in the rational numbers. -/
+def ofInt (num : Int) : Rat := { num, reduced := Nat.coprime_one_right _ }
+
+instance : NatCast Rat where
+  natCast n := ofInt n
+instance : IntCast Rat := ⟨ofInt⟩
+
+instance : OfNat Rat n := ⟨n⟩
+
+/-- Is this rational number integral? -/
+@[inline] protected def isInt (a : Rat) : Bool := a.den == 1
+
+/-- Form the quotient `n / d` where `n d : Int`. -/
+def divInt : Int → Int → Rat
+  | n, .ofNat d => inline (mkRat n d)
+  | n, .negSucc d => normalize (-n) d.succ nofun
+
+@[inherit_doc] scoped infixl:70 " /. " => Rat.divInt
+
+/-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is
+`@[irreducible]` because you don't want to unfold it. Use `Rat.ofScientific_def`,
+`Rat.ofScientific_true_def`, or `Rat.ofScientific_false_def` instead.) -/
+@[irreducible] protected def ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat :=
+  if s then
+    Rat.normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pow_pos (by decide)
+  else
+    (m * 10 ^ e : Nat)
+
+instance : OfScientific Rat where
+  ofScientific m s e := Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e)
+
+/-- Rational number strictly less than relation, as a `Bool`. -/
+protected def blt (a b : Rat) : Bool :=
+  if a.num < 0 && 0 ≤ b.num then
+    true
+  else if a.num = 0 then
+    0 < b.num
+  else if 0 < a.num && b.num ≤ 0 then
+    false
+  else
+    -- `a` and `b` must have the same sign
+   a.num * b.den < b.num * a.den
+
+instance : LT Rat := ⟨(·.blt ·)⟩
+
+instance (a b : Rat) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (_ = true))
+
+instance : LE Rat := ⟨fun a b => b.blt a = false⟩
+
+instance (a b : Rat) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (_ = false))
+
+/-- 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 :=
+  let g1 := Nat.gcd a.num.natAbs b.den
+  let g2 := Nat.gcd b.num.natAbs a.den
+  { num := a.num.divExact g1 (normalize.dvd_num rfl) * b.num.divExact g2 (normalize.dvd_num rfl)
+    den := a.den.divExact g2 (normalize.dvd_den rfl) * b.den.divExact g1 (normalize.dvd_den rfl)
+    den_nz := Nat.ne_of_gt <| Nat.mul_pos
+      (Nat.div_gcd_pos_of_pos_right _ a.den_pos) (Nat.div_gcd_pos_of_pos_right _ b.den_pos)
+    reduced := by
+      simp only [Int.divExact_eq_tdiv, Int.natAbs_mul, Int.natAbs_tdiv, Nat.coprime_mul_iff_left]
+      refine ⟨Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩, Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩⟩
+      · exact a.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
+          |>.coprime_div_right (Nat.gcd_dvd_right ..)
+      · exact Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ b.den_pos)
+      · exact Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ a.den_pos)
+      · exact b.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
+          |>.coprime_div_right (Nat.gcd_dvd_right ..) }
+
+instance : Mul Rat := ⟨Rat.mul⟩
+
+/--
+The inverse of a rational number. Note: `inv 0 = 0`. (This definition is `@[irreducible]`
+because you don't want to unfold it. Use `Rat.inv_def` instead.)
+-/
+@[irreducible] protected def inv (a : Rat) : Rat :=
+  if h : a.num < 0 then
+    { num := -a.den, den := a.num.natAbs
+      den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_lt h))
+      reduced := Int.natAbs_neg a.den ▸ a.reduced.symm }
+  else if h : a.num > 0 then
+    { num := a.den, den := a.num.natAbs
+      den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_gt h))
+      reduced := a.reduced.symm }
+  else
+    a
+
+/-- Division of rational numbers. Note: `div a 0 = 0`. -/
+protected def div : Rat → Rat → Rat := (· * ·.inv)
+
+/-- Division of rational numbers. Note: `div a 0 = 0`.  Written with a separate function `Rat.div`
+as a wrapper so that the definition is not unfolded at `.instance` transparency. -/
+instance : Div Rat := ⟨Rat.div⟩
+
+theorem add.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
+    (had : ad = a.den / g) (hbd : bd = b.den / g) :
+    let den := ad * b.den; let num := a.num * bd + b.num * ad
+    num.natAbs.gcd g = num.natAbs.gcd den := by
+  intro den num
+  have ae : ad * g = a.den := had ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_left ..)
+  have be : bd * g = b.den := hbd ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_right ..)
+  have hden : den = ad * bd * g := by rw [Nat.mul_assoc, be]
+  rw [hden, Nat.Coprime.gcd_mul_left_cancel_right]
+  have cop : ad.Coprime bd := had ▸ hbd ▸ hg ▸
+    Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_left _ a.den_pos)
+  have H1 (d : Nat) :
+      d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad := by
+    have := d.gcd_dvd_right num.natAbs
+    rw [← Int.ofNat_dvd, Int.dvd_natAbs] at this
+    have := Int.dvd_iff_dvd_of_dvd_add this
+    rwa [← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul,
+      ← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul] at this
+  apply Nat.Coprime.mul_left
+  · have := (H1 ad).2 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
+    have := (cop.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
+    exact Nat.eq_one_of_dvd_one <| a.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
+      Nat.dvd_trans (Nat.gcd_dvd_left ..) (ae ▸ Nat.dvd_mul_right ..)
+  · have := (H1 bd).1 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
+    have := (cop.symm.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
+    exact Nat.eq_one_of_dvd_one <| b.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
+      Nat.dvd_trans (Nat.gcd_dvd_left ..) (be ▸ Nat.dvd_mul_right ..)
+
+/--
+Addition of rational numbers. (This definition is `@[irreducible]` because you don't want to
+unfold it. Use `Rat.add_def` instead.)
+-/
+@[irreducible] protected def add (a b : Rat) : Rat :=
+  let g := a.den.gcd b.den
+  if hg : g = 1 then
+    have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos
+    have reduced := add.aux a b hg.symm (Nat.div_one _).symm (Nat.div_one _).symm
+      |>.symm.trans (Nat.gcd_one_right _)
+    { num := a.num * b.den + b.num * a.den, den := a.den * b.den, den_nz, reduced }
+  else
+    let den := (a.den / g) * b.den
+    let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g)
+    let g1  := num.natAbs.gcd g
+    have den_nz := Nat.ne_of_gt <| Nat.mul_pos (Nat.div_gcd_pos_of_pos_left _ a.den_pos) b.den_pos
+    have e : g1 = num.natAbs.gcd den := add.aux a b rfl rfl rfl
+    Rat.maybeNormalize num den g1 (normalize.dvd_num e) (normalize.dvd_den e)
+      (normalize.den_nz den_nz e) (normalize.reduced den_nz e)
+
+instance : Add Rat := ⟨Rat.add⟩
+
+/-- Negation of rational numbers. -/
+protected def neg (a : Rat) : Rat :=
+  { a with num := -a.num, reduced := by rw [Int.natAbs_neg]; exact a.reduced }
+
+instance : Neg Rat := ⟨Rat.neg⟩
+
+theorem sub.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
+    (had : ad = a.den / g) (hbd : bd = b.den / g) :
+    let den := ad * b.den; let num := a.num * bd - b.num * ad
+    num.natAbs.gcd g = num.natAbs.gcd den := by
+  have := add.aux a (-b) hg had hbd
+  simp only [show (-b).num = -b.num from rfl, Int.neg_mul] at this
+  exact this
+
+/-- Subtraction of rational numbers. (This definition is `@[irreducible]` because you don't want to
+unfold it. Use `Rat.sub_def` instead.)
+-/
+@[irreducible] protected def sub (a b : Rat) : Rat :=
+  let g := a.den.gcd b.den
+  if hg : g = 1 then
+    have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos
+    have reduced := sub.aux a b hg.symm (Nat.div_one _).symm (Nat.div_one _).symm
+      |>.symm.trans (Nat.gcd_one_right _)
+    { num := a.num * b.den - b.num * a.den, den := a.den * b.den, den_nz, reduced }
+  else
+    let den := (a.den / g) * b.den
+    let num := a.num * ↑(b.den / g) - b.num * ↑(a.den / g)
+    let g1  := num.natAbs.gcd g
+    have den_nz := Nat.ne_of_gt <| Nat.mul_pos (Nat.div_gcd_pos_of_pos_left _ a.den_pos) b.den_pos
+    have e : g1 = num.natAbs.gcd den := sub.aux a b rfl rfl rfl
+    Rat.maybeNormalize num den g1 (normalize.dvd_num e) (normalize.dvd_den e)
+      (normalize.den_nz den_nz e) (normalize.reduced den_nz e)
+
+instance : Sub Rat := ⟨Rat.sub⟩
+
+/-- The floor of a rational number `a` is the largest integer less than or equal to `a`. -/
+protected def floor (a : Rat) : Int :=
+  if a.den = 1 then
+    a.num
+  else
+    a.num / a.den
+
+/-- The ceiling of a rational number `a` is the smallest integer greater than or equal to `a`. -/
+protected def ceil (a : Rat) : Int :=
+  if a.den = 1 then
+    a.num
+  else
+    a.num / a.den + 1
+
+end Rat

src/Init/Data/Rat/Lemmas.lean

@@ -0,0 +1,388 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+module
+prelude
+
+public import Init.Data.Rat.Basic
+
+@[expose] public section
+
+/-! # Additional lemmas about the Rational Numbers -/
+
+namespace Rat
+
+-- This is not marked as an `@[ext]` lemma as this is rarely useful for rational numbers.
+theorem ext : {p q : Rat} → p.num = q.num → p.den = q.den → p = q
+  | ⟨_,_,_,_⟩, ⟨_,_,_,_⟩, rfl, rfl => rfl
+
+@[simp] theorem mk_den_one {r : Int} :
+    ⟨r, 1, Nat.one_ne_zero, (Nat.coprime_one_right _)⟩ = (r : Rat) := rfl
+
+@[simp] theorem zero_num : (0 : Rat).num = 0 := rfl
+@[simp] theorem zero_den : (0 : Rat).den = 1 := rfl
+@[simp] theorem one_num : (1 : Rat).num = 1 := rfl
+@[simp] theorem one_den : (1 : Rat).den = 1 := rfl
+
+@[simp] theorem maybeNormalize_eq {num den g} (dvd_num dvd_den den_nz reduced) :
+    maybeNormalize num den g dvd_num dvd_den den_nz reduced =
+    { num := num.divExact g dvd_num, den := den / g, den_nz, reduced } := by
+  unfold maybeNormalize; split
+  · subst g; simp
+  · rfl
+
+theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
+    { num := num / num.natAbs.gcd den
+      den := den / num.natAbs.gcd den
+      den_nz := normalize.den_nz den_nz rfl
+      reduced := normalize.reduced den_nz rfl } := by
+  simp only [normalize, maybeNormalize_eq, Int.divExact_eq_ediv]
+
+@[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
+
+theorem mk_eq_normalize (num den nz c) : ⟨num, den, nz, c⟩ = normalize num den nz := by
+  simp [normalize_eq, c.gcd_eq_one]
+
+theorem normalize_self (r : Rat) : normalize r.num r.den r.den_nz = r := (mk_eq_normalize ..).symm
+
+theorem normalize_mul_left {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
+    normalize (↑a * n) (a * d) (Nat.mul_ne_zero a0 d0) = normalize n d d0 := by
+  simp [normalize_eq, Int.natAbs_mul, Nat.gcd_mul_left,
+    Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero a0), Int.natCast_mul,
+    Int.mul_ediv_mul_of_pos _ _ (Int.natCast_pos.2 <| Nat.pos_of_ne_zero a0)]
+
+theorem normalize_mul_right {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
+    normalize (n * a) (d * a) (Nat.mul_ne_zero d0 a0) = normalize n d d0 := by
+  rw [← normalize_mul_left (d0 := d0) a0]
+  congr 1
+  · apply Int.mul_comm
+  · apply Nat.mul_comm
+
+theorem normalize_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    normalize n₁ d₁ z₁ = normalize n₂ d₂ z₂ ↔ n₁ * d₂ = n₂ * d₁ := by
+  constructor <;> intro h
+  · simp only [normalize_eq, mk'.injEq] at h
+    have hn₁ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₁.natAbs d₁
+    have hn₂ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₂.natAbs d₂
+    have hd₁ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₁.natAbs d₁
+    have hd₂ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₂.natAbs d₂
+    rw [← Int.ediv_mul_cancel (Int.dvd_trans hd₂ (Int.dvd_mul_left ..)),
+      Int.mul_ediv_assoc _ hd₂, ← Int.natCast_ediv, ← h.2, Int.natCast_ediv,
+      ← Int.mul_ediv_assoc _ hd₁, Int.mul_ediv_assoc' _ hn₁,
+      Int.mul_right_comm, h.1, Int.ediv_mul_cancel hn₂]
+  · rw [← normalize_mul_right _ z₂, ← normalize_mul_left z₂ z₁, Int.mul_comm d₁, h]
+
+theorem maybeNormalize_eq_normalize {num : Int} {den g : Nat} (dvd_num dvd_den den_nz reduced)
+    (hn : ↑g ∣ num) (hd : g ∣ den) :
+    maybeNormalize num den g dvd_num dvd_den den_nz reduced =
+      normalize num den (mt (by simp [·]) den_nz) := by
+  simp only [maybeNormalize_eq, mk_eq_normalize, Int.divExact_eq_ediv]
+  have : g ≠ 0 := mt (by simp [·]) den_nz
+  rw [← normalize_mul_right _ this, Int.ediv_mul_cancel hn]
+  congr 1; exact Nat.div_mul_cancel hd
+
+@[simp] theorem normalize_eq_zero (d0 : d ≠ 0) : normalize n d d0 = 0 ↔ n = 0 := by
+  have' := normalize_eq_iff d0 Nat.one_ne_zero
+  rw [normalize_zero (d := 1)] at this; rw [this]; simp
+
+theorem normalize_num_den' (num den nz) : ∃ d : Nat, d ≠ 0 ∧
+    num = (normalize num den nz).num * d ∧ den = (normalize num den nz).den * d := by
+  refine ⟨num.natAbs.gcd den, Nat.gcd_ne_zero_right nz, ?_⟩
+  simp [normalize_eq, Int.ediv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..),
+    Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
+
+theorem normalize_num_den (h : normalize n d z = ⟨n', d', z', c⟩) :
+    ∃ m : Nat, m ≠ 0 ∧ n = n' * m ∧ d = d' * m := by
+  have := normalize_num_den' n d z; rwa [h] at this
+
+theorem normalize_eq_mkRat {num den} (den_nz) : normalize num den den_nz = mkRat num den := by
+  simp [mkRat, den_nz]
+
+theorem mkRat_num_den (z : d ≠ 0) (h : mkRat n d = ⟨n', d', z', c⟩) :
+    ∃ m : Nat, m ≠ 0 ∧ n = n' * m ∧ d = d' * m :=
+  normalize_num_den ((normalize_eq_mkRat z).symm ▸ h)
+
+theorem mkRat_def (n d) : mkRat n d = if d0 : d = 0 then 0 else normalize n d d0 := rfl
+
+theorem mkRat_self (a : Rat) : mkRat a.num a.den = a := by
+  rw [← normalize_eq_mkRat a.den_nz, normalize_self]
+
+theorem mk_eq_mkRat (num den nz c) : ⟨num, den, nz, c⟩ = mkRat num den := by
+  simp [mk_eq_normalize, normalize_eq_mkRat]
+
+@[simp] theorem zero_mkRat (n) : mkRat 0 n = 0 := by simp [mkRat_def]
+
+@[simp] theorem mkRat_zero (n) : mkRat n 0 = 0 := by simp [mkRat_def]
+
+theorem mkRat_eq_zero (d0 : d ≠ 0) : mkRat n d = 0 ↔ n = 0 := by simp [mkRat_def, d0]
+
+theorem mkRat_ne_zero (d0 : d ≠ 0) : mkRat n d ≠ 0 ↔ n ≠ 0 := not_congr (mkRat_eq_zero d0)
+
+theorem mkRat_mul_left {a : Nat} (a0 : a ≠ 0) : mkRat (↑a * n) (a * d) = mkRat n d := by
+  if d0 : d = 0 then simp [d0] else
+  rw [← normalize_eq_mkRat d0, ← normalize_mul_left d0 a0, normalize_eq_mkRat]
+
+theorem mkRat_mul_right {a : Nat} (a0 : a ≠ 0) : mkRat (n * a) (d * a) = mkRat n d := by
+  rw [← mkRat_mul_left (d := d) a0]
+  congr 1
+  · apply Int.mul_comm
+  · apply Nat.mul_comm
+
+theorem mkRat_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁ := by
+  rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_eq_iff]
+
+@[simp] theorem divInt_ofNat (num den) : num /. (den : Nat) = mkRat num den := by
+  simp [divInt]
+
+theorem mk_eq_divInt (num den nz c) : ⟨num, den, nz, c⟩ = num /. (den : Nat) := by
+  simp [mk_eq_mkRat]
+
+theorem divInt_self (a : Rat) : a.num /. a.den = a := by rw [divInt_ofNat, mkRat_self]
+
+@[simp] theorem zero_divInt (n) : 0 /. n = 0 := by cases n <;> simp [divInt]
+
+@[simp] theorem divInt_zero (n) : n /. 0 = 0 := mkRat_zero n
+
+theorem neg_divInt_neg (num den) : -num /. -den = num /. den := by
+  match den with
+  | Nat.succ n =>
+    simp only [divInt, Int.neg_ofNat_succ]
+    simp [normalize_eq_mkRat, Int.neg_neg]
+  | 0 => rfl
+  | Int.negSucc n =>
+    simp only [divInt, Int.neg_negSucc]
+    simp [normalize_eq_mkRat]
+
+theorem divInt_neg' (num den) : num /. -den = -num /. den := by rw [← neg_divInt_neg, Int.neg_neg]
+
+theorem divInt_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁ := by
+  rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
+  rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
+  simp_all [divInt_neg', Int.neg_eq_zero,
+    mkRat_eq_iff, Int.neg_mul, Int.mul_neg, Int.eq_neg_comm, eq_comm]
+
+theorem divInt_mul_left {a : Int} (a0 : a ≠ 0) : (a * n) /. (a * d) = n /. d := by
+  if d0 : d = 0 then simp [d0] else
+  simp [divInt_eq_iff (Int.mul_ne_zero a0 d0) d0, Int.mul_assoc, Int.mul_left_comm]
+
+theorem divInt_mul_right {a : Int} (a0 : a ≠ 0) : (n * a) /. (d * a) = n /. d := by
+  simp [← divInt_mul_left (d := d) a0, Int.mul_comm]
+
+theorem divInt_num_den (z : d ≠ 0) (h : n /. d = ⟨n', d', z', c⟩) :
+    ∃ m, m ≠ 0 ∧ n = n' * m ∧ d = d' * m := by
+  rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;>
+    simp_all [divInt_neg', Int.neg_eq_zero]
+  · have ⟨m, h₁, h₂⟩ := mkRat_num_den z h; exists m
+    simp [Int.natCast_mul, h₁, h₂]
+  · have ⟨m, h₁, h₂⟩ := mkRat_num_den z h; exists -m
+    rw [← Int.neg_inj, Int.neg_neg] at h₂
+    simp [Int.natCast_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]
+
+@[simp] theorem ofInt_ofNat : ofInt (OfNat.ofNat n) = OfNat.ofNat n := rfl
+
+@[simp] theorem ofInt_num : (ofInt n : Rat).num = n := rfl
+@[simp] theorem ofInt_den : (ofInt n : Rat).den = 1 := rfl
+
+@[simp] theorem ofNat_num : (OfNat.ofNat n : Rat).num = OfNat.ofNat n := rfl
+@[simp] theorem ofNat_den : (OfNat.ofNat n : Rat).den = 1 := rfl
+
+theorem add_def (a b : Rat) :
+    a + b = normalize (a.num * b.den + b.num * a.den) (a.den * b.den)
+      (Nat.mul_ne_zero a.den_nz b.den_nz) := by
+  show Rat.add .. = _; delta Rat.add; dsimp only; split
+  · exact (normalize_self _).symm
+  · have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz
+    rw [maybeNormalize_eq_normalize _ _ _ _
+        (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)
+        (Nat.dvd_trans (Nat.gcd_dvd_right ..) <|
+         Nat.dvd_trans (Nat.gcd_dvd_right ..) (Nat.dvd_mul_left ..)),
+      ← normalize_mul_right _ this]; congr 1
+    · simp only [Int.add_mul, Int.mul_assoc, Int.ofNat_mul_ofNat,
+        Nat.div_mul_cancel (Nat.gcd_dvd_left ..), Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
+    · rw [Nat.mul_right_comm, Nat.div_mul_cancel (Nat.gcd_dvd_left ..)]
+
+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]
+
+theorem normalize_add_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
+    normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ =
+    normalize (n₁ * d₂ + n₂ * d₁) (d₁ * d₂) (Nat.mul_ne_zero z₁ z₂) := by
+  cases e₁ : normalize n₁ d₁ z₁; rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩
+  cases e₂ : normalize n₂ d₂ z₂; rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩
+  simp only [add_def]; rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]; congr 1
+  · rw [Int.add_mul]; simp [Int.natCast_mul, Int.mul_assoc, Int.mul_left_comm, Int.mul_comm]
+  · simp [Nat.mul_left_comm, Nat.mul_comm]
+
+theorem mkRat_add_mkRat (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * d₂ + n₂ * d₁) (d₁ * d₂) := by
+  rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_add_normalize, normalize_eq_mkRat]
+
+theorem divInt_add_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂) := by
+  rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
+  rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
+  simp_all [← Int.natCast_mul, Int.neg_eq_zero, divInt_neg', Int.mul_neg,
+    Int.neg_add, Int.neg_mul, mkRat_add_mkRat]
+
+@[simp] theorem neg_num (a : Rat) : (-a).num = -a.num := rfl
+@[simp] theorem neg_den (a : Rat) : (-a).den = a.den := rfl
+
+theorem neg_normalize (n d z) : -normalize n d z = normalize (-n) d z := by
+  simp only [normalize, maybeNormalize_eq, Int.divExact_eq_tdiv, Int.natAbs_neg, Int.neg_tdiv]
+  rfl
+
+theorem neg_mkRat (n d) : -mkRat n d = mkRat (-n) d := by
+  if z : d = 0 then simp [z]; rfl else simp [← normalize_eq_mkRat z, neg_normalize]
+
+theorem neg_divInt (n d) : -(n /. d) = -n /. d := by
+  rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;> simp [divInt_neg', neg_mkRat]
+
+theorem sub_def (a b : Rat) :
+    a - b = normalize (a.num * b.den - b.num * a.den) (a.den * b.den)
+      (Nat.mul_ne_zero a.den_nz b.den_nz) := by
+  show Rat.sub .. = _; delta Rat.sub; dsimp only; split
+  · exact (normalize_self _).symm
+  · have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz
+    rw [maybeNormalize_eq_normalize _ _ _ _
+        (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)
+        (Nat.dvd_trans (Nat.gcd_dvd_right ..) <|
+         Nat.dvd_trans (Nat.gcd_dvd_right ..) (Nat.dvd_mul_left ..)),
+      ← normalize_mul_right _ this]; congr 1
+    · simp only [Int.sub_mul, Int.mul_assoc, ← Int.natCast_mul,
+        Nat.div_mul_cancel (Nat.gcd_dvd_left ..), Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
+    · rw [Nat.mul_right_comm, Nat.div_mul_cancel (Nat.gcd_dvd_left ..)]
+
+theorem sub_def' (a b : Rat) : a - b = mkRat (a.num * b.den - b.num * a.den) (a.den * b.den) := by
+  rw [sub_def, normalize_eq_mkRat]
+
+protected theorem sub_eq_add_neg (a b : Rat) : a - b = a + -b := by
+  simp [add_def, sub_def, Int.neg_mul, Int.sub_eq_add_neg]
+
+theorem divInt_sub_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
+    n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂) := by
+  simp only [Rat.sub_eq_add_neg, neg_divInt,
+    divInt_add_divInt _ _ z₁ z₂, Int.neg_mul, Int.sub_eq_add_neg]
+
+theorem mul_def (a b : Rat) :
+    a * b = normalize (a.num * b.num) (a.den * b.den) (Nat.mul_ne_zero a.den_nz b.den_nz) := by
+  show Rat.mul .. = _; delta Rat.mul; dsimp only
+  have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
+  have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
+  simp only [Int.divExact_eq_tdiv, Nat.divExact_eq_div]
+  rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]; congr 1
+  · rw [Int.natCast_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
+  · rw [← Nat.mul_assoc, Nat.mul_right_comm, Nat.mul_right_comm (_/_),
+      Nat.div_mul_cancel (Nat.gcd_dvd_right ..), Nat.mul_assoc,
+      Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
+
+theorem mul_def' (a b : Rat) : a * b = mkRat (a.num * b.num) (a.den * b.den) := by
+  rw [mul_def, normalize_eq_mkRat]
+
+protected theorem mul_comm (a b : Rat) : a * b = b * a := by
+  simp [mul_def, normalize_eq_mkRat, Int.mul_comm, Nat.mul_comm]
+
+@[simp] protected theorem zero_mul (a : Rat) : 0 * a = 0 := by simp [mul_def]
+@[simp] protected theorem mul_zero (a : Rat) : a * 0 = 0 := by simp [mul_def]
+@[simp] protected theorem one_mul (a : Rat) : 1 * a = a := by simp [mul_def, normalize_self]
+@[simp] protected theorem mul_one (a : Rat) : a * 1 = a := by simp [mul_def, normalize_self]
+
+theorem normalize_mul_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
+    normalize n₁ d₁ z₁ * normalize n₂ d₂ z₂ =
+    normalize (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero z₁ z₂) := by
+  cases e₁ : normalize n₁ d₁ z₁; rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩
+  cases e₂ : normalize n₂ d₂ z₂; rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩
+  simp only [mul_def]; rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]; congr 1
+  · simp [Int.natCast_mul, Int.mul_assoc, Int.mul_left_comm]
+  · simp [Nat.mul_left_comm, Nat.mul_comm]
+
+theorem mkRat_mul_mkRat (n₁ n₂ : Int) (d₁ d₂) :
+    mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂) := by
+  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) :
+    (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⟩ <;>
+  simp_all [← Int.natCast_mul, divInt_neg', Int.mul_neg, Int.neg_mul, mkRat_mul_mkRat]
+
+theorem inv_def (a : Rat) : a.inv = (a.den : Int) /. a.num := by
+  unfold Rat.inv; split
+  · next h => rw [mk_eq_divInt, ← Int.natAbs_neg,
+      Int.natAbs_of_nonneg (Int.le_of_lt <| Int.neg_pos_of_neg h), neg_divInt_neg]
+  split
+  · next h => rw [mk_eq_divInt, Int.natAbs_of_nonneg (Int.le_of_lt h)]
+  · next h₁ h₂ =>
+    apply (divInt_self _).symm.trans
+    simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]
+
+@[simp] protected theorem inv_zero : (0 : Rat).inv = 0 := by unfold Rat.inv; rfl
+
+@[simp] theorem inv_divInt (n d : Int) : (n /. d).inv = d /. n := by
+  if z : d = 0 then simp [z] else
+  cases e : n /. d; rcases divInt_num_den z e with ⟨g, zg, rfl, rfl⟩
+  simp [inv_def, divInt_mul_right zg]
+
+theorem div_def (a b : Rat) : a / b = a * b.inv := rfl
+
+/-! ### `ofScientific` -/
+
+theorem ofScientific_true_def : Rat.ofScientific m true e = mkRat m (10 ^ e) := by
+  unfold Rat.ofScientific; rw [normalize_eq_mkRat]; rfl
+
+theorem ofScientific_false_def : Rat.ofScientific m false e = (m * 10 ^ e : Nat) := by
+  unfold Rat.ofScientific; rfl
+
+theorem ofScientific_def : Rat.ofScientific m s e =
+    if s then mkRat m (10 ^ e) else (m * 10 ^ e : Nat) := by
+  cases s; exact ofScientific_false_def; exact ofScientific_true_def
+
+/-- `Rat.ofScientific` applied to numeric literals is the same as a scientific literal. -/
+@[simp]
+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 intCast_den (a : Int) : (a : Rat).den = 1 := rfl
+
+@[simp] theorem intCast_num (a : Int) : (a : Rat).num = a := rfl
+
+/-!
+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`.
+-/
+
+@[simp, norm_cast] theorem intCast_inj {a b : Int} : (a : Rat) = (b : Rat) ↔ a = b := by
+  constructor
+  · rintro ⟨⟩; rfl
+  · simp_all
+
+theorem intCast_zero : ((0 : Int) : Rat) = (0 : Rat) := rfl
+
+theorem intCast_one : ((1 : Int) : Rat) = (1 : Rat) := rfl
+
+@[simp, norm_cast] 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 intCast_neg (a : Int) : ((-a : Int) : Rat) = -(a : Rat) := rfl
+
+@[simp, norm_cast] theorem intCast_sub (a b : Int) :
+    ((a - b : Int) : Rat) = (a : Rat) - (b : Rat) := by
+  rw [sub_def]
+  simp [normalize_eq]
+
+@[simp, norm_cast] theorem intCast_mul (a b : Int) :
+    ((a * b : Int) : Rat) = (a : Rat) * (b : Rat) := by
+  rw [mul_def]
+  simp [normalize_eq]

tests/lean/hpow.lean

@@ -1,5 +1,3 @@
-import Std.Internal.Rat
-open Std.Internal
 
 /-!
 Test the `rightact%` elaborator for `HPow.hPow`, added to address #2854
@@ -15,7 +13,7 @@ variable (n : Nat) (m : Int) (q : Rat)
 #check (n ^ 2 + (1 : Nat) : Int)
 
 instance instNatPowRat : NatPow Rat where
-  pow q n := Std.Internal.mkRat (q.num ^ n) (q.den ^ n)
+  pow q n := mkRat (q.num ^ n) (q.den ^ n)
 
 instance instPowRatInt : Pow Rat Int where
   pow q m := if 0 ≤ m then q ^ (m.toNat : Nat) else (1/q) ^ ((-m).toNat)

tests/lean/rat1.lean

@@ -1,5 +1,3 @@
-import Std.Internal.Rat
-open Std.Internal
 open Lean
 
 #eval (15 : Rat) / 10

tests/lean/run/Rat.lean

@@ -1,6 +1,3 @@
-import Std.Internal.Rat
-
-open Std.Internal
 
 /-- info: 1 -/
 #guard_msgs in

tests/lean/run/grind_cutsat_cooper.lean

@@ -1,4 +1,4 @@
-import Std.Internal.Rat
+
 example (x y : Int) :
     27 ≤ 11*x + 13*y →
     11*x + 13*y ≤ 45 →

tests/lean/run/ppNumericTypes.lean

@@ -1,5 +1,3 @@
-import Std.Internal.Rat
-open Std.Internal
 
 /-!
 Tests for `pp.numericTypes` and `pp.natLit`

tests/lean/run/rational.lean

@@ -1,44 +1,44 @@
-structure Rat where
+structure Rat' where
   num : Int
   den : Nat
   pos : den > 0
 
-instance (n : Nat) : OfNat Rat n where
+instance (n : Nat) : OfNat Rat' n where
   ofNat := {
     num := n
     den := 1
     pos := by decide
   }
 
-instance : Add Rat where
+instance : Add Rat' where
   add a b := {
     num := a.num * b.den + b.num * a.den
     den := a.den * b.den
     pos := sorry
   }
 
-instance : NatCast Rat where
+instance : NatCast Rat' where
   natCast n := {
     num := n
     den := 1
     pos := by decide
   }
 
-instance : IntCast Rat where
+instance : IntCast Rat' where
   intCast n := {
     num := n
     den := 1
     pos := by decide
   }
 
-def f1 (x : Rat) (n : Nat) : Rat :=
+def f1 (x : Rat') (n : Nat) : Rat' :=
   x + n + 1
 
-def f2 (x : Rat) (n : Nat) : Rat :=
+def f2 (x : Rat') (n : Nat) : Rat' :=
   1 + x + n
 
-def f3 (x : Rat) (n : Nat) : Rat :=
+def f3 (x : Rat') (n : Nat) : Rat' :=
   1 + n + x + 2
 
-def f4 (x : Rat) (n : Nat) : Rat :=
+def f4 (x : Rat') (n : Nat) : Rat' :=
   n + 1 + x + n