Theorem: Equiv.Perm.ofSubtype_mem_stabilizer' (Jordan/StabilizerPrimitive.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g • s ⊆ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ Set.Finite s

State before:
case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ Set.Finite s
Tactic:
exact s.toFinite
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
⊢ ofSubtype g • s ⊆ s
Tactic:
intro x
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s
Tactic:
rw [Set.mem_smul_set]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s
Tactic:
rintro ⟨y, hy, rfl⟩
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ ofSubtype g • y ∈ s
Tactic:
simp only [Equiv.Perm.smul_def]
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ (ofSubtype g) y ∈ s
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem g (Set.not_mem_compl_iff.mpr hy)]
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ y ∈ s

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑sᶜ
y : α
hy : y ∈ s
⊢ y ∈ s
Tactic:
exact hy
State after:
no goals