no goals
α : Type u_1
β : Type ?u.181036
γ : Type ?u.181039
δ : Type ?u.181042
inst✝ : CommMonoid α
a₁ a₂ b₁ b₂ : α
c₁ : αˣ
h₁ : a₁ * ↑c₁ = b₁
c₂ : αˣ
h₂ : a₂ * ↑c₂ = b₂
⊢ a₁ * a₂ * ↑(c₁ * c₂) = b₁ * b₂
simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]