Theorem: MulAction.stabilizer_subgroupOf_eq (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
⊢ stabilizer (↥N) a = Subgroup.subgroupOf (stabilizer G a) N
Tactic:
ext n
State after:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n ∈ stabilizer (↥N) a ↔ n ∈ Subgroup.subgroupOf (stabilizer G a) N

State before:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n ∈ stabilizer (↥N) a ↔ n ∈ Subgroup.subgroupOf (stabilizer G a) N
Tactic:
simp only [Subgroup.mem_subgroupOf, mem_stabilizer_iff]
State after:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n • a = a ↔ ↑n • a = a

State before:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n • a = a ↔ ↑n • a = a
Tactic:
rfl
State after:
no goals