Theorem: Equiv.Perm.stabilizer_ne_top (Jordan/PermMaximal.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤
Tactic:
obtain ⟨a, ha⟩ := hs
State after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hsc : Set.Nonempty sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (Perm α) s ≠ ⊤

State before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hsc : Set.Nonempty sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (Perm α) s ≠ ⊤
Tactic:
obtain ⟨b, hb⟩ := hsc
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤
Tactic:
intro h
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : stabilizer (Perm α) s = ⊤
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : stabilizer (Perm α) s = ⊤
⊢ False
Tactic:
rw [Set.mem_compl_iff] at hb
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ False
Tactic:
apply hb
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ b ∈ s

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ b ∈ s
Tactic:
have hg : Equiv.swap a b ∈ stabilizer (Equiv.Perm α) s := by rw [h]; apply Subgroup.mem_top
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b ∈ stabilizer (Perm α) s
⊢ b ∈ s

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b ∈ stabilizer (Perm α) s
⊢ b ∈ s
Tactic:
rw [mem_stabilizer_iff] at hg
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ b ∈ s

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ b ∈ s
Tactic:
rw [← hg]
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ b ∈ swap a b • s

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ b ∈ swap a b • s
Tactic:
rw [Set.mem_smul_set]
State after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ ∃ y ∈ s, swap a b • y = b

State before:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ ∃ y ∈ s, swap a b • y = b
Tactic:
use a
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ a ∈ s ∧ swap a b • a = b

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ a ∈ s ∧ swap a b • a = b
Tactic:
use ha
State after:
case right
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ swap a b • a = b

State before:
case right
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ swap a b • a = b
Tactic:
apply Equiv.swap_apply_left
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ swap a b ∈ stabilizer (Perm α) s
Tactic:
rw [h]
State after:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ swap a b ∈ ⊤

State before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ swap a b ∈ ⊤
Tactic:
apply Subgroup.mem_top
State after:
no goals