[GOAL]
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
[PROOFSTEP]
simpa using h 1
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
q : SubMulAction R M
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
carrier✝¹ : Set M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ carrier✝¹ → c • x ∈ carrier✝¹
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h :
  { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ { x // x ∈ p } →[R] M
[PROOFSTEP]
refine' { toFun := Subtype.val .. }
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : { x // x ∈ p }), ↑(m • x) = m • ↑x
[PROOFSTEP]
simp [val_smul]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p
[PROOFSTEP]
rw [← one_smul R x, ← smul_assoc]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p
[PROOFSTEP]
exact p.smul_mem _ h
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
x✝ : R
⊢ x✝ ∈ MulAction.Stabilizer.submonoid R m ↔ x✝ ∈ MulAction.Stabilizer.submonoid R ↑m
[PROOFSTEP]
simp only [MulAction.mem_stabilizer_submonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m
[PROOFSTEP]
rw [← Subgroup.toSubmonoid_eq]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
[PROOFSTEP]
exact stabilizer_of_subMul.submonoid m
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
hx : x ∈ p
⊢ -x ∈ p
[PROOFSTEP]
rw [← neg_one_smul R]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
hx : x ∈ p
⊢ -1 • x ∈ p
[PROOFSTEP]
exact p.smul_mem _ hx
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
h : -x ∈ p
⊢ x ∈ p
[PROOFSTEP]
rw [← neg_neg x]
[GOAL]
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : SubMulAction R M
r : R
x y : M
h : -x ∈ p
⊢ - -x ∈ p
[PROOFSTEP]
exact neg_mem _ h
