case a
p q✝ q : ℚ≥0
⊢ ↑(↑(num q) / ↑(den q)) = ↑q
p q✝ q : ℚ≥0
⊢ ↑(num q) / ↑(den q) = q
ext1
case a
p q✝ q : ℚ≥0
⊢ ↑(↑q).num / ↑(den q) = ↑q
case a
p q✝ q : ℚ≥0
⊢ ↑(↑(num q) / ↑(den q)) = ↑q
rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_ofNat,
  Int.natAbs_of_nonneg (Rat.num_nonneg_iff_zero_le.2 q.prop)]
no goals
case a
p q✝ q : ℚ≥0
⊢ ↑(↑q).num / ↑(den q) = ↑q
exact Rat.num_div_den q