a b c p q : ℚ
⊢ p.num /. ↑p.den = q.num /. ↑q.den ↔ p.num * ↑q.den = q.num * ↑p.den
a b c p q : ℚ
⊢ p = q ↔ p.num * ↑q.den = q.num * ↑p.den
conv =>
  lhs
  rw [← @num_den p, ← @num_den q]
case z₂
a b c p q : ℚ
⊢ ¬q.den = 0
case z₂
a b c p q : ℚ
⊢ ↑q.den ≠ 0
rw [← Nat.cast_zero, Ne, Int.ofNat_inj]
no goals
case z₂
a b c p q : ℚ
⊢ ¬q.den = 0
apply den_nz