no goals
n d : ℤ
⊢ (n /. d).num = Int.sign d * n / ↑(Int.gcd n d)
rcases d with ((_ | _) | _) <;>
rw [←Int.div_eq_ediv_of_dvd] <;>
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ,
  Int.zero_ediv, Int.ofNat_dvd_left, Nat.gcd_dvd_left]