α : Type u
β : Type v
x✝ x y : FreeMagma α
hx : FreeSemigroup.length (↑toFreeSemigroup x) = length x
hy : FreeSemigroup.length (↑toFreeSemigroup y) = length y
⊢ length x + length y = length (x * y)
α : Type u
β : Type v
x✝ x y : FreeMagma α
hx : FreeSemigroup.length (↑toFreeSemigroup x) = length x
hy : FreeSemigroup.length (↑toFreeSemigroup y) = length y
⊢ FreeSemigroup.length (↑toFreeSemigroup (x * y)) = length (x * y)
rw [map_mul, FreeSemigroup.length_mul, hx, hy]
no goals
α : Type u
β : Type v
x✝ x y : FreeMagma α
hx : FreeSemigroup.length (↑toFreeSemigroup x) = length x
hy : FreeSemigroup.length (↑toFreeSemigroup y) = length y
⊢ length x + length y = length (x * y)
rfl