no goals
α : Type u
β : Type v
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
f : α → β
hf : IsMonoidHom f
γ : Type u_1
inst✝ : MulOneClass γ
g : β → γ
hg : IsMonoidHom g
src✝ : IsMulHom (g ∘ f) := IsMulHom.comp hf.toIsMulHom hg.toIsMulHom
⊢ g (f 1) = 1
rw [hf.map_one, hg.map_one]