num : Int
den : Nat
nz : den ≠ 0
⊢ num = (normalize num den).num * ↑(Nat.gcd (Int.natAbs num) den) ∧
    den = (normalize num den).den * Nat.gcd (Int.natAbs num) den
num : Int
den : Nat
nz : den ≠ 0
⊢ ∃ d, d ≠ 0 ∧ num = (normalize num den).num * ↑d ∧ den = (normalize num den).den * d
refine ⟨num.natAbs.gcd den, Nat.gcd_ne_zero_right nz, ?_⟩
no goals
num : Int
den : Nat
nz : den ≠ 0
⊢ num = (normalize num den).num * ↑(Nat.gcd (Int.natAbs num) den) ∧
    den = (normalize num den).den * Nat.gcd (Int.natAbs num) den
simp [normalize_eq, Int.ediv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..),
  Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]