∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] {s : Set M} {m : M} [Nontrivial R],
  (MonoidAlgebra.of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(MonoidAlgebra.of R M) '' s)) →
    m ∈ Submonoid.closure s