case h.e'_1
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ ↑r.num / ↑↑r.den = r
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ p (↑r.num / ↑↑r.den)
convert hr
no goals
case h.e'_1
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ ↑r.num / ↑↑r.den = r
convert num_div_den r