feat: num and den lemmas (#10219)

Add a few basic lemmas about `Rat` and `NNRat` and fix some lemma names

From LeanAPAP

Mathlib/Algebra/Order/Archimedean.lean

@@ -297,10 +297,10 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
   · rw [Rat.coe_int_den, Nat.cast_one]
     exact one_ne_zero
   · intro H
-    rw [Rat.coe_nat_num, Int.cast_ofNat, Nat.cast_eq_zero] at H
+    rw [Rat.num_natCast, Int.cast_ofNat, Nat.cast_eq_zero] at H
     subst H
     cases n0
-  · rw [Rat.coe_nat_den, Nat.cast_one]
+  · rw [Rat.den_natCast, Nat.cast_one]
     exact one_ne_zero
 #align exists_rat_btwn exists_rat_btwn
 

Mathlib/Data/Int/Defs.lean

@@ -19,6 +19,9 @@ open Nat
 namespace Int
 variable {m n : ℕ}
 
+-- TODO: Tag in Std
+attribute [simp] natAbs_pos
+
 instance instNontrivialInt : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩
 
 @[simp] lemma ofNat_eq_cast : Int.ofNat n = n := rfl

Mathlib/Data/Rat/Defs.lean

@@ -44,6 +44,11 @@ theorem ofInt_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
   rfl
 #align rat.of_int_eq_cast Rat.ofInt_eq_cast
 
+-- TODO: Replace `Rat.ofNat_num`/`Rat.ofNat_den` in Std
+-- See note [no_index around OfNat.ofNat]
+@[simp] lemma num_ofNat (n : ℕ) : num (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+@[simp] lemma den_ofNat (n : ℕ) : den (no_index (OfNat.ofNat n)) = 1 := rfl
+
 @[simp, norm_cast]
 theorem coe_int_num (n : ℤ) : (n : ℚ).num = n :=
   rfl
@@ -531,15 +536,15 @@ theorem coe_nat_eq_divInt (n : ℕ) : ↑n = n /. 1 := by
   rw [← Int.cast_ofNat, coe_int_eq_divInt]
 #align rat.coe_nat_eq_mk Rat.coe_nat_eq_divInt
 
-@[simp, norm_cast]
-theorem coe_nat_num (n : ℕ) : (n : ℚ).num = n := by
-  rw [← Int.cast_ofNat, coe_int_num]
-#align rat.coe_nat_num Rat.coe_nat_num
+@[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl
+#align rat.coe_nat_num Rat.num_natCast
 
-@[simp, norm_cast]
-theorem coe_nat_den (n : ℕ) : (n : ℚ).den = 1 := by
-  rw [← Int.cast_ofNat, coe_int_den]
-#align rat.coe_nat_denom Rat.coe_nat_den
+@[simp, norm_cast] lemma den_natCast (n : ℕ) : den n = 1 := rfl
+#align rat.coe_nat_denom Rat.den_natCast
+
+-- TODO: Fix the names in Std
+alias num_intCast := intCast_num
+alias den_intCast := intCast_den
 
 -- Will be subsumed by `Int.coe_inj` after we have defined
 -- `LinearOrderedField ℚ` (which implies characteristic zero).

Mathlib/Data/Rat/NNRat.lean

@@ -394,25 +394,30 @@ namespace NNRat
 variable {p q : ℚ≥0}
 
 /-- The numerator of a nonnegative rational. -/
-def num (q : ℚ≥0) : ℕ :=
-  (q : ℚ).num.natAbs
+@[pp_dot] def num (q : ℚ≥0) : ℕ := (q : ℚ).num.natAbs
 #align nnrat.num NNRat.num
 
 /-- The denominator of a nonnegative rational. -/
-def den (q : ℚ≥0) : ℕ :=
-  (q : ℚ).den
+@[pp_dot] def den (q : ℚ≥0) : ℕ := (q : ℚ).den
 #align nnrat.denom NNRat.den
 
-@[simp]
-theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num :=
-  rfl
+@[norm_cast] lemma num_coe (q : ℚ≥0) : (q : ℚ).num = q.num := by
+  simp [num, abs_of_nonneg, Rat.num_nonneg_iff_zero_le.2 q.2]
+
+theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num := rfl
 #align nnrat.nat_abs_num_coe NNRat.natAbs_num_coe
 
-@[simp]
-theorem den_coe : (q : ℚ).den = q.den :=
-  rfl
+@[simp, 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 _
+
+-- 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
+@[simp, norm_cast] lemma den_natCast (n : ℕ) : den n = 1 := rfl
+
 theorem ext_num_den (hn : p.num = q.num) (hd : p.den = q.den) : p = q := by
   ext
   · apply (Int.natAbs_inj_of_nonneg_of_nonneg _ _).1 hn