From ff5ae592fc73de179b382c49f1f6c700587f99f8 Mon Sep 17 00:00:00 2001
From: Daniel Weber <55664973+Command-Master@users.noreply.github.com>
Date: Thu, 2 May 2024 20:30:22 +0300
Subject: [PATCH] Fix sorry in `NNRat.cast_divNat` (#7)

---
 LeanAPAP/Mathlib/Data/Rat/Cast/CharZero.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/LeanAPAP/Mathlib/Data/Rat/Cast/CharZero.lean b/LeanAPAP/Mathlib/Data/Rat/Cast/CharZero.lean
index f8c4cd5c8b..8c0d0d9617 100644
--- 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