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

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

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

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

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

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

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

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

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

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

State before:
case intro.intro
α✝ : Type ?u.27969
inst✝³ : DecidableEq α✝
G : Type ?u.27981
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
g : Perm α := swap a b
h' : g • s = s
⊢ b ∈ g • s
Tactic:
use a
State after:
case h
α✝ : Type ?u.27969
inst✝³ : DecidableEq α✝
G : Type ?u.27981
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
g : Perm α := swap a b
h' : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = b

State before:
case h
α✝ : Type ?u.27969
inst✝³ : DecidableEq α✝
G : Type ?u.27981
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
g : Perm α := swap a b
h' : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = b
Tactic:
exact And.intro ha (Equiv.swap_apply_left a b)
State after:
no goals