∀ {M : Type u_2} {N : Type u_1} [inst : Monoid M] [inst_1 : Monoid N] {s : Set M} (f : M → N),
  Submonoid.closure s = ⊤ → f 1 = 1 → (∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y) → ∀ (x y : M), f (x * y) = f x * f y