case h
α : Type u
β : Type v
f : α → β
⊢ ↑(MulHom.comp toFreeSemigroup (map f)) ∘ of = ↑(MulHom.comp (FreeSemigroup.map f) toFreeSemigroup) ∘ of
α : Type u
β : Type v
f : α → β
⊢ MulHom.comp toFreeSemigroup (map f) = MulHom.comp (FreeSemigroup.map f) toFreeSemigroup
ext1
no goals
case h
α : Type u
β : Type v
f : α → β
⊢ ↑(MulHom.comp toFreeSemigroup (map f)) ∘ of = ↑(MulHom.comp (FreeSemigroup.map f) toFreeSemigroup) ∘ of
rfl