refactor(Rat): Streamline basic theory (#11504)

`Rat` has a long history in (and before) mathlib and as such its development is full of cruft. Now that `NNRat` is a thing, there is a need for the theory of `Rat` to be mimickable to yield the theory of `NNRat`, which is not currently the case.

Broadly, this PR aims at mirroring the `Rat` and `NNRat` declarations. It achieves this by:
* Relying more on `Rat.num` and `Rat.den`, and less on the structure representation of `Rat`
* Abandoning the vestigial `Rat.Nonneg` (which was replaced in Std by a new development of the order on `Rat`)
* Renaming many `Rat` lemmas with dubious names. This creates quite a lot of conflicts with Std lemmas, whose names are themselves dubious. I am priming the relevant new mathlib names and leaving TODOs to fix the Std names.
* Handling most of the `Rat` porting notes

Reduce the diff of #11203

Author: YaelDillies

Mathlib/Algebra/Order/Archimedean.lean

@@ -302,8 +302,6 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
     rw [Rat.num_natCast, Int.cast_natCast, Nat.cast_eq_zero] at H
     subst H
     cases n0
-  · rw [Rat.den_natCast, Nat.cast_one]
-    exact one_ne_zero
 #align exists_rat_btwn exists_rat_btwn
 
 theorem le_of_forall_rat_lt_imp_le (h : ∀ q : ℚ, (q : α) < x → (q : α) ≤ y) : x ≤ y :=

Mathlib/Algebra/Order/Nonneg/Field.lean

@@ -22,6 +22,7 @@ This is used to derive algebraic structures on `ℝ≥0` and `ℚ≥0` automatic
 * `{x : α // 0 ≤ x}` is a `CanonicallyLinearOrderedSemifield` if `α` is a `LinearOrderedField`.
 -/
 
+assert_not_exists abs_inv
 
 open Set
 

Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -3,11 +3,10 @@ Copyright (c) 2022 Yaël Dillies, George Shakan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, George Shakan
 -/
+import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Data.Finset.Pointwise
-import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Tactic.GCongr
-import Mathlib.Algebra.GroupPower.Order
 
 #align_import combinatorics.additive.pluennecke_ruzsa from "leanprover-community/mathlib"@"4aab2abced69a9e579b1e6dc2856ed3db48e2cbd"
 

Mathlib/Combinatorics/SimpleGraph/Density.lean

@@ -8,6 +8,7 @@ import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Data.Rat.Cast.Order
 import Mathlib.Order.Partition.Finpartition
 import Mathlib.Tactic.GCongr
+import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Ring
 

Mathlib/Data/NNRat/Defs.lean

@@ -30,30 +30,18 @@ of `x` with `↑x`. This tactic also works for a function `f : α → ℚ` with
 
 open Function
 
-/-- Nonnegative rational numbers. -/
-def NNRat := { q : ℚ // 0 ≤ q } deriving
-  CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedAddCommMonoid, Sub, Inhabited
-#align nnrat NNRat
+deriving instance CanonicallyOrderedCommSemiring for NNRat
+deriving instance CanonicallyLinearOrderedAddCommMonoid for NNRat
+deriving instance Sub for NNRat
+deriving instance Inhabited for NNRat
 
--- Porting note (#10754): Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
--- instead of `deriving` them
-instance : OrderedSub NNRat := Nonneg.orderedSub
-
-scoped[NNRat] notation "ℚ≥0" => NNRat
+-- TODO: `deriving instance OrderedSub for NNRat` doesn't work yet, so we add the instance manually
+instance NNRat.instOrderedSub : OrderedSub ℚ≥0 := Nonneg.orderedSub
 
 namespace NNRat
 
 variable {α : Type*} {p q : ℚ≥0}
 
-instance instCoe : Coe ℚ≥0 ℚ := ⟨Subtype.val⟩
-
-/-
--- Simp lemma to put back `n.val` into the normal form given by the coercion.
-@[simp]
-theorem val_eq_coe (q : ℚ≥0) : q.val = q :=
-  rfl
--/
--- Porting note: `val_eq_coe` is no longer needed.
 #noalign nnrat.val_eq_coe
 
 instance canLift : CanLift ℚ ℚ≥0 (↑) fun q ↦ 0 ≤ q where
@@ -358,26 +346,21 @@ namespace NNRat
 
 variable {p q : ℚ≥0}
 
-/-- The numerator of a nonnegative rational. -/
-@[pp_dot] def num (q : ℚ≥0) : ℕ := (q : ℚ).num.natAbs
-#align nnrat.num NNRat.num
-
-/-- The denominator of a nonnegative rational. -/
-@[pp_dot] def den (q : ℚ≥0) : ℕ := (q : ℚ).den
-#align nnrat.denom NNRat.den
-
 @[norm_cast] lemma num_coe (q : ℚ≥0) : (q : ℚ).num = q.num := by
   simp [num, abs_of_nonneg, Rat.num_nonneg, q.2]
 
 theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num := rfl
 #align nnrat.nat_abs_num_coe NNRat.natAbs_num_coe
 
-@[simp, norm_cast] lemma den_coe : (q : ℚ).den = q.den := rfl
+@[norm_cast] lemma den_coe : (q : ℚ).den = q.den := rfl
 #align nnrat.denom_coe NNRat.den_coe
 
 @[simp] lemma num_ne_zero : q.num ≠ 0 ↔ q ≠ 0 := by simp [num]
 @[simp] lemma num_pos : 0 < q.num ↔ 0 < q := by simp [pos_iff_ne_zero]
 @[simp] lemma den_pos (q : ℚ≥0) : 0 < q.den := Rat.den_pos _
+@[simp] lemma den_ne_zero (q : ℚ≥0) : q.den ≠ 0 := Rat.den_ne_zero _
+
+lemma coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den := by simpa [num, den] using Rat.reduced _
 
 -- TODO: Rename `Rat.coe_nat_num`, `Rat.intCast_den`, `Rat.ofNat_num`, `Rat.ofNat_den`
 @[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl
@@ -395,7 +378,34 @@ theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=
   ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun h ↦ ext_num_den h.1 h.2⟩
 #align nnrat.ext_num_denom_iff NNRat.ext_num_den_iff
 
-end NNRat
+/-- Form the quotient `n / d` where `n d : ℕ`.
 
--- `NNRat` needs to be available in the definition of `Field`
-assert_not_exists Field
+See also `Rat.divInt` and `mkRat`. -/
+def divNat (n d : ℕ) : ℚ≥0 := ⟨.divInt n d, Rat.divInt_nonneg n.cast_nonneg d.cast_nonneg⟩
+
+variable {n₁ n₂ d₁ d₂ d : ℕ}
+
+@[simp, norm_cast] lemma coe_divNat (n d : ℕ) : (divNat n d : ℚ) = .divInt n d := rfl
+
+lemma mk_divInt (n d : ℕ) :
+    ⟨.divInt n d, Rat.divInt_nonneg n.cast_nonneg d.cast_nonneg⟩ = divNat n d := rfl
+
+lemma divNat_inj (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁ := by
+  rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast
+
+@[simp] lemma num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q :=
+  ext $ by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe]
+
+/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with nonnegative rational
+numbers of the form `n / d` with `d ≠ 0` and `n`, `d` coprime. -/
+@[elab_as_elim]
+def numDenCasesOn.{u} {C : ℚ≥0 → Sort u} (q) (H : ∀ n d, d ≠ 0 → n.Coprime d → C (divNat n d)) :
+    C q := by rw [← q.num_divNat_den]; exact H _ _ q.den_ne_zero q.coprime_num_den
+
+lemma add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den) := by
+  ext; simp [Rat.add_def', Rat.mkRat_eq, num_coe, den_coe]
+
+lemma mul_def (q r : ℚ≥0) : q * r = divNat (q.num * r.num) (q.den * r.den) := by
+  ext; simp [Rat.mul_def', Rat.mkRat_eq, num_coe, den_coe]
+
+end NNRat

Mathlib/Data/NNRat/Lemmas.lean

@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Function.Indicator
-import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Algebra.Order.Nonneg.Field
-import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.Rat.Field
 
 #align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
@@ -21,20 +18,9 @@ cycles.
 open Function
 open scoped NNRat
 
--- The `LinearOrderedCommGroupWithZero` instance is a shortcut instance for performance
-deriving instance CanonicallyLinearOrderedSemifield, LinearOrderedCommGroupWithZero for NNRat
-
 namespace NNRat
 variable {α : Type*} {p q : ℚ≥0}
 
-instance instDenselyOrdered : DenselyOrdered ℚ≥0 := Nonneg.instDenselyOrdered
-
-@[simp, norm_cast] lemma coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹ := rfl
-#align nnrat.coe_inv NNRat.coe_inv
-
-@[simp, norm_cast] lemma coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q := rfl
-#align nnrat.coe_div NNRat.coe_div
-
 /-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
 instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
   MulAction.compHom α coeHom.toMonoidHom

Mathlib/Data/Nat/Digits.lean

@@ -598,7 +598,7 @@ theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1
   cases b
   · rw [digits_def' one_lt_two]
     · simpa [Nat.bit, Nat.bit0_val n]
-    · simpa [pos_iff_ne_zero, bit_eq_zero_iff]
+    · simpa [pos_iff_ne_zero, Nat.bit0_eq_zero]
   · simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
 #align nat.digits_two_eq_bits Nat.digits_two_eq_bits
 

Mathlib/Data/Rat/Cast/CharZero.lean

@@ -31,12 +31,12 @@ theorem cast_inj [CharZero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
     refine' ⟨fun h => _, congr_arg _⟩
     have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
     have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
-    rw [num_den', num_den'] at h ⊢
-    rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h <;> simp [d₁0, d₂0] at h ⊢
-    rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
-      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
-      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj,
-      ← mkRat_eq_iff d₁0 d₂0] at h
+    rw [mk'_eq_divInt, mk'_eq_divInt] at h ⊢
+    rw [cast_divInt_of_ne_zero, cast_divInt_of_ne_zero] at h <;> simp [d₁0, d₂0] at h ⊢
+    rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq, ←
+      mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁, ←
+      Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
+      at h
 #align rat.cast_inj Rat.cast_inj
 
 theorem cast_injective [CharZero α] : Function.Injective ((↑) : ℚ → α)