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