no goals
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (↑a * n) (a * d) = normalize n d
simp [normalize_eq, mk'.injEq, Int.natAbs_mul, Nat.gcd_mul_left,
  Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero a0), Int.ofNat_mul,
  Int.mul_ediv_mul_of_pos _ _ (Int.ofNat_pos.2 <| Nat.pos_of_ne_zero a0)]