internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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]
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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]
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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]
Proof 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 ∈ ⊤
Theorem: Equiv.Perm.stabilizer_ne_top
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_empty_eq_top
Proof state before:
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G ∅ = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G ∅
Theorem: Equiv.Perm.stabilizer_empty_eq_top
Proof state before:
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G ∅
Tactic:
intro g
Proof state after:
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G ∅
Theorem: Equiv.Perm.stabilizer_empty_eq_top
Proof state before:
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G ∅
Tactic:
apply imp_intro
Proof state after:
case h
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G ∅
Theorem: Equiv.Perm.stabilizer_empty_eq_top
Proof state before:
case h
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G ∅
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case h
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • ∅ = ∅
Theorem: Equiv.Perm.stabilizer_empty_eq_top
Proof state before:
case h
α✝ : Type ?u.23342
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.23354
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • ∅ = ∅
Tactic:
simp only [Set.smul_set_empty]
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_univ_eq_top
Proof state before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G _root_.Set.univ = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G _root_.Set.univ
Theorem: Equiv.Perm.stabilizer_univ_eq_top
Proof state before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ ⊤ ≤ stabilizer G _root_.Set.univ
Tactic:
intro g
Proof state after:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G _root_.Set.univ
Theorem: Equiv.Perm.stabilizer_univ_eq_top
Proof state before:
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ ⊤ → g ∈ stabilizer G _root_.Set.univ
Tactic:
apply imp_intro
Proof state after:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G _root_.Set.univ
Theorem: Equiv.Perm.stabilizer_univ_eq_top
Proof state before:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g ∈ stabilizer G _root_.Set.univ
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • _root_.Set.univ = _root_.Set.univ
Theorem: Equiv.Perm.stabilizer_univ_eq_top
Proof state before:
case h
α✝ : Type ?u.25282
inst✝⁵ : DecidableEq α✝
G✝ : Type ?u.25294
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α✝
inst✝² : Fintype α✝
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
⊢ g • _root_.Set.univ = _root_.Set.univ
Tactic:
simp only [Set.smul_set_univ]
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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 ≠ ⊤
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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'
Proof 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 ≠ ⊤
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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'
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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']
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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
Proof 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
Theorem: Equiv.Perm.stabilizer_nonempty_ne_top
Proof 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)
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
have : ∀ (t : Set α) (_ : 1 < t.ncard), ∃ (g : Equiv.Perm α),
    g.IsSwap ∧ g ∈ stabilizer (Equiv.Perm α) t := by
  intro t ht
  rw [Set.one_lt_ncard_iff] at ht
  obtain ⟨a, b, ha, hb, h⟩ := ht
  simp only [Ne.def, Subtype.mk_eq_mk] at h
  use Equiv.swap a b
  constructor
  rw [swap_isSwap_iff]; exact h
  apply swap_mem_stabilizer ha hb
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
⊢ ∃ g, IsSwap g ∧ g ∈ G
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases' lt_or_le 1 (s.ncard) with h1 h1'
Proof state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
⊢ ∃ g, IsSwap g ∧ g ∈ G

case inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases' lt_or_le 1 sᶜ.ncard with h1c h1c'
Proof state after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
⊢ ∃ g, IsSwap g ∧ g ∈ G

case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases subgroup_of_group_of_order_two (by
  rw [Fintype.card_perm, ← Nat.card_eq_fintype_card, hα]
  simp) G with
| inl h =>
  exfalso; exact ne_bot_of_gt hG h
| inr h =>
  rw [h]
  rw [← stabilizer_univ_eq_top (Equiv.Perm α) α]
  apply this
  rw [Set.ncard_univ, hα]
  norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
intro t ht
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < Set.ncard t
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < Set.ncard t
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
rw [Set.one_lt_ncard_iff] at ht
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : ∃ a b, a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : ∃ a b, a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
obtain ⟨a, b, ha, hb, h⟩ := ht
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t