no goals
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeSemigroup α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : ↑f (of x) = ↑g (of x)
hy : ↑f y = ↑g y
⊢ ↑f (of x * y) = ↑g (of x * y)
simp only [map_mul, *]