q : ℚ
⊢ Nat.coprime (Int.natAbs q.num * Int.natAbs q.num) (q.den * q.den)
q : ℚ
⊢ (q * q).den = q.den * q.den
rw [Rat.mul_den, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Nat.div_one]
no goals
q : ℚ
⊢ Nat.coprime (Int.natAbs q.num * Int.natAbs q.num) (q.den * q.den)
exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)