∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : AddSubmonoid M)
  (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier), ↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S