chore(Data/Rat/Lemmas): deprecate num_mk and den_mk (leanprover-community#33334)

Author: SnirBroshi

Mathlib/Data/Rat/Lemmas.lean

@@ -56,19 +56,13 @@ theorem num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) :
     rw [qdf]
     exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)
 
-theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d := by
-  have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
-    rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_natCast]
-  rcases d with ((_ | _) | _) <;>
-  simp [divInt, mkRat, Rat.normalize_eq, Int.sign, Int.gcd,
-    Int.zero_ediv, this]
-
-theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d := by
-  have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
-    rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_natCast]
-  rcases d with ((_ | _) | _) <;>
-    simp [divInt, mkRat, Rat.normalize_eq, Int.gcd,
-      if_neg (Nat.cast_add_one_ne_zero _), this]
+@[deprecated Rat.num_divInt (since := "2025-12-27")]
+theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d :=
+  Int.gcd_comm .. ▸ Rat.num_divInt ..
+
+@[deprecated Rat.den_divInt (since := "2025-12-27")]
+theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d :=
+  Int.gcd_comm .. ▸ Rat.den_divInt ..
 
 theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den := by
   rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)