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:
α : 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
Tactic:
intro x
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ x ∈ ofSubtype g • s → x ∈ s

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

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

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite 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

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
x : α
⊢ (∃ y ∈ s, ofSubtype g • y = x) → x ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite 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

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite 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

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite 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

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite 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

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem g hy]
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ↑(g { val := y, property := hy }) ∈ s

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

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
y : α
hy : y ∈ s
⊢ ↑(g { val := y, property := hy }) ∈ s

case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
g : Perm ↑s
⊢ Set.Finite s
Tactic:
refine' Subtype.mem _
State after:
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