have : qn ≃ 0 ∧ qd ≃ 0 := And.intro ‹qn ≃ 0› ‹qd ≃ 0›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁷ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁶ : pn * qd ≃ qn * pd
this✝⁵ : qn * rd ≃ rn * qd
this✝⁴ : qn * pd ≃ 0
this✝³ : qn * rd ≃ 0
this✝² : qn ≃ 0 ∨ pd ≃ 0
this✝¹ : qn ≃ 0 ∨ rd ≃ 0
this✝ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁸ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁷ : pn * qd ≃ qn * pd
this✝⁶ : qn * rd ≃ rn * qd
this✝⁵ : qn * pd ≃ 0
this✝⁴ : qn * rd ≃ 0
this✝³ : qn ≃ 0 ∨ pd ≃ 0
this✝² : qn ≃ 0 ∨ rd ≃ 0
this✝¹ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
this : qn ≃ 0 ∧ qd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)