no goals
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2
rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
    ← mul_assoc n2, mul_comm n2, mul_assoc, h2]