no goals
α : Type u
β : Type v
inst✝² : Mul α
inst✝¹ : Mul β
γ : Type u_1
inst✝ : Mul γ
f : α → β
g : β → γ
hf : IsMulHom f
hg : IsMulHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
simp only [Function.comp, hf.map_mul, hg.map_mul]