Theorem: MulAction.Nat.Combination.stabilizer_eq (Jordan/PermMaximal.lean)

State before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
⊢ stabilizer G s = stabilizer G ↑↑s
Tactic:
ext g
State after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g ∈ stabilizer G s ↔ g ∈ stabilizer G ↑↑s

State before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g ∈ stabilizer G s ↔ g ∈ stabilizer G ↑↑s
Tactic:
simp only [mem_stabilizer_iff]
State after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g • s = s ↔ g • ↑↑s = ↑↑s

State before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g • s = s ↔ g • ↑↑s = ↑↑s
Tactic:
rw [← Subtype.coe_inj, ← Finset.coe_smul_finset]
State after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑(g • s) = ↑s ↔ ↑(g • ↑s) = ↑↑s

State before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑(g • s) = ↑s ↔ ↑(g • ↑s) = ↑↑s
Tactic:
simp only [← Finset.coe_smul_finset, ← Finset.coe_inj]
State after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑↑(g • s) = ↑↑s ↔ ↑(g • ↑s) = ↑↑s

State before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑↑(g • s) = ↑↑s ↔ ↑(g • ↑s) = ↑↑s
Tactic:
simp only [Nat.combination_mulAction.coe_apply', Finset.coe_smul_finset]
State after:
no goals