no goals
α : Type u_1
β : Type ?u.22031
γ : Type ?u.22034
M : Type u_2
inst✝¹ : Monoid M
N : Type ?u.22043
inst✝ : Monoid N
f g : FreeMonoid α →* M
h : ∀ (x : α), ↑f (of x) = ↑g (of x)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : ↑f xs = ↑g xs
⊢ ↑f (of x * xs) = ↑g (of x * xs)
simp only [h, hxs, MonoidHom.map_mul]