∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (s : Set M), Submonoid.map f (Submonoid.closure s) = Submonoid.closure (⇑f '' s)