q : ℚ
⊢ Nat.coprime (Int.natAbs q.num * Int.natAbs q.num) (q.den * q.den)
q : ℚ
⊢ (q * q).num = q.num * q.num
rw [mul_num, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_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)