match this with
| isTrue (_ : qd ≃ 0) =>
  have : pn * qd ≃ qn * pd := ‹pn//pd ≃ qn//qd›
  have : qn * rd ≃ rn * qd := ‹qn//qd ≃ rn//rd›
  have : qn * pd ≃ 0 := calc
    qn * pd ≃ _ := Rel.symm ‹pn * qd ≃ qn * pd›
    pn * qd ≃ _ := AA.substR ‹qd ≃ 0›
    pn * 0  ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : qn * rd ≃ 0 := calc
    qn * rd ≃ _ := ‹qn * rd ≃ rn * qd›
    rn * qd ≃ _ := AA.substR ‹qd ≃ 0›
    rn * 0  ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : qn ≃ 0 ∨ pd ≃ 0 := Integer.mul_split_zero.mp ‹qn * pd ≃ 0›
  have : qn ≃ 0 ∨ rd ≃ 0 := Integer.mul_split_zero.mp ‹qn * rd ≃ 0›
  have : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0) :=
    And.intro ‹qn ≃ 0 ∨ pd ≃ 0› ‹qn ≃ 0 ∨ rd ≃ 0›
  have : qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0) :=
    Logic.or_distribL_and.mpr ‹(qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)›
  match ‹qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0)› with
  | Or.inl (_ : qn ≃ 0) =>
    have : qn ≃ 0 ∧ qd ≃ 0 := And.intro ‹qn ≃ 0› ‹qd ≃ 0›
    have : (qn, qd) ≃ (0, 0) :=
      Relation.Equivalence.Impl.Prod.eqv_defn.mpr ‹qn ≃ 0 ∧ qd ≃ 0›
    exact Or.inr ‹(qn, qd) ≃ (0, 0)›
  | Or.inr (And.intro (_ : pd ≃ 0) (_ : rd ≃ 0)) =>
    have : pn * rd ≃ rn * pd := calc
      pn * rd ≃ _ := AA.substR ‹rd ≃ 0›
      pn * 0  ≃ _ := AA.absorbR
      0       ≃ _ := Rel.symm AA.absorbR
      rn * 0  ≃ _ := AA.substR (Rel.symm ‹pd ≃ 0›)
      rn * pd ≃ _ := Rel.refl
    exact Or.inl ‹pn * rd ≃ rn * pd›
| isFalse (_ : qd ≄ 0) =>
  have : pn * rd ≃ rn * pd :=
    eqv_trans_nonzero_denom
      (q := qn//qd)
      ‹qd ≄ 0›
      ‹pn//pd ≃ qn//qd›
      ‹qn//qd ≃ rn//rd›
  exact Or.inl ‹pn * rd ≃ rn * pd›
ℕ : 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)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
no goals