∀ {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] {ι : Sort u_5} (f : F) (s : ι → Submonoid M),
  Submonoid.map f (iSup s) = ⨆ i, Submonoid.map f (s i)