have : p₁n * p₂d ≃ p₂n * p₁d := ‹p₁n//p₁d ≃ p₂n//p₂d›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)