a b c q : ℚ
hq : q.num = 0
this : q = q.num /. ↑q.den
⊢ q = 0
a b c q : ℚ
hq : q.num = 0
⊢ q = 0
have : q = q.num /. q.den := num_den.symm
no goals
a b c q : ℚ
hq : q.num = 0
this : q = q.num /. ↑q.den
⊢ q = 0
simpa [hq] using this