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