calc
  (p₁n * qd + p₁d * qn) * (p₂d * qd)
    ≃ _ := Rel.symm AA.assoc
  ((p₁n * qd + p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL AA.distribR
  ((p₁n * qd) * p₂d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (AA.substL AA.comm))
  ((qd * p₁n) * p₂d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL AA.assoc)
  (qd * (p₁n * p₂d) + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (AA.substR ‹p₁n * p₂d ≃ p₂n * p₁d›))
  (qd * (p₂n * p₁d) + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (Rel.symm AA.assoc))
  ((qd * p₂n) * p₁d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substR AA.assoc)
  ((qd * p₂n) * p₁d + p₁d * (qn * p₂d)) * qd
    ≃ _ := AA.substL (AA.substR AA.comm)
  ((qd * p₂n) * p₁d + (qn * p₂d) * p₁d) * qd
    ≃ _ := AA.substL (Rel.symm AA.distribR)
  ((qd * p₂n + qn * p₂d) * p₁d) * qd
    ≃ _ := AA.assoc
  (qd * p₂n + qn * p₂d) * (p₁d * qd)
    ≃ _ := AA.substL (AA.substL AA.comm)
  (p₂n * qd + qn * p₂d) * (p₁d * qd)
    ≃ _ := AA.substL (AA.substR AA.comm)
  (p₂n * qd + p₂d * qn) * (p₁d * qd)
    ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
no goals