Update Mathlib/Data/Rat/Lemmas.lean

Co-authored-by: Bhavik Mehta <[email protected]>
leanprover-community · Dec 11, 2024 · d58b085 · d58b085
1 parent b0d3512
commit d58b085
Showing 1 changed file with 8 additions and 13 deletions.
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
@@ -64,19 +64,14 @@ theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gc
       if_neg (Nat.cast_add_one_ne_zero _), this]
 
 theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den := by
-  rw [Rat.add_def, Rat.normalize_eq,
-    Nat.div_dvd_iff_dvd_mul
-      (Nat.gcd_dvd_right _ _)
-      (Nat.gcd_ne_zero_right (mul_ne_zero (Rat.den_ne_zero _) (Rat.den_ne_zero _))),
-    ← Nat.gcd_mul_lcm,
-    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (Rat.den_ne_zero _) (Rat.den_ne_zero _)),
-    Nat.dvd_gcd_iff]
-  constructor
-  · rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
-    apply Int.dvd_add
-      <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
-      <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]
-  · exact dvd_mul_right _ _
+  rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
+    (Nat.gcd_ne_zero_right (by simp)), ← Nat.gcd_mul_lcm,
+    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]
+  refine ⟨?_, dvd_mul_right _ _⟩
+  rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
+  apply Int.dvd_add
+    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
+    <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]
 
 theorem add_den_dvd (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den * q₂.den := by
   rw [add_def, normalize_eq]