Fix sorry in NNRat.cast_divNat (#7)

YaelDillies · May 2, 2024 · ff5ae59 · ff5ae59
1 parent 3ec222d
commit ff5ae59
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/LeanAPAP/Mathlib/Data/Rat/Cast/CharZero.lean b/LeanAPAP/Mathlib/Data/Rat/Cast/CharZero.lean
@@ -53,7 +53,11 @@ lemma cast_zpow (q : ℚ≥0) (n : ℤ) : ↑(q ^ n) = ((q : α) ^ n : α) := ma
 @[simp, norm_cast] lemma cast_div (p q) : (p / q : ℚ≥0) = (p / q : α) := map_div₀ (castHom α) _ _
 
 @[simp, norm_cast]
-lemma cast_divNat (a b : ℕ) : (divNat a b : α) = a / b := sorry
+lemma cast_divNat (a b : ℕ) : (divNat a b : α) = a / b := by
+  rw [← cast_natCast, ← cast_natCast b, ← cast_div]
+  congr
+  ext
+  apply Rat.mkRat_eq_div
 
 end DivisionSemiring
 end NNRat