no goals
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ * (n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₂ /. ↑d₂ * (n₃ /. ↑d₃))
simp [h₁, h₂, h₃, mul_ne_zero, mul_comm, mul_assoc, mul_left_comm]