no goals
α : Type u
β : Type v
f : α → β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : length (↑(map f) (of x)) = length (of x)
hy : length (↑(map f) y) = length y
⊢ length (↑(map f) (of x * y)) = length (of x * y)
simp only [map_mul, length_mul, *]