no goals
S✝ : Type u'
T : Type u''
R✝ : Type u
M✝ : Type v
inst✝⁵ : SMul R✝ M✝
inst✝⁴ : SetLike S✝ M✝
hS : SMulMemClass S✝ R✝ M✝
s : S✝
R : Type u_1
M : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : SetLike S M
inst✝ : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N
simpa using h 1