no goals
num : Int
den : Nat
den_nz : den ≠ 0
⊢ normalize num den = mk' (num / ↑(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)
simp only [normalize, maybeNormalize_eq,
  Int.div_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]