no goals
n₁ n₂ d₁ d₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂)
rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
simp_all [Int.ofNat_eq_zero, Int.neg_eq_zero, divInt_neg', Int.mul_neg,
  Int.ofNat_mul_ofNat, Int.neg_add, Int.neg_mul, mkRat_add_mkRat]