no goals
α✝ : Type u
β✝ : Type v
inst✝⁴ : Mul α✝
inst✝³ : Mul β✝
γ : Type ?u.931
inst✝² : Mul γ
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : CommSemigroup β
f g : α → β
hf : IsMulHom f
hg : IsMulHom g
a b : α
⊢ f (a * b) * g (a * b) = f a * g a * (f b * g b)
simp only [hf.map_mul, hg.map_mul, mul_comm, mul_assoc, mul_left_comm]