internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ stabilizer (↥(alternatingGroup α)) s
Tactic:
erw [h]
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤
Tactic:
apply Subgroup.mem_top
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
⊢ a ≠ c
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ False
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ False
Tactic:
apply hc
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ c ∈ s
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ c ∈ s
Tactic:
rw [← h]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ a ∈ s
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ a ∈ s
Tactic:
exact ha
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
⊢ a ≠ b
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ False
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ False
Tactic:
apply hb
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ b ∈ s
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ b ∈ s
Tactic:
rw [← h]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ a ∈ s
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ a ∈ s
Tactic:
exact ha
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ g ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.sign g = 1
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.sign g = 1
Tactic:
apply Equiv.Perm.IsThreeCycle.sign
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.IsThreeCycle g
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.IsThreeCycle g
Tactic:
apply Equiv.Perm.isThreeCycle_swap_mul_swap_same hab hac hbc
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ s
Tactic:
rw [← this]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ g • s
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ g • s
Tactic:
use a
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = c
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = c
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Tactic:
exact ha
Proof state after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Tactic:
dsimp [g]
Proof state after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) ((Equiv.swap a c) a) = c
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) ((Equiv.swap a c) a) = c
Tactic:
rw [Equiv.swap_apply_left]
Proof state after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) c = c
Theorem: alternatingGroup.stabilizer_ne_top'
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) c = c
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hac.symm hbc.symm]
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hssc : Set.Nontrivial s ∨ Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
cases' hssc with hs' hsc'
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hsc' : Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top
Proof state before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hsc' : Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
exact stabilizer_ne_top' s hs hsc'
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
rw [← stabilizer_compl]
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial s
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Tactic:
rw [← compl_compl s] at hs'
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial sᶜᶜ
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
hs' : Set.Nontrivial sᶜᶜ
⊢ stabilizer (↥(alternatingGroup α)) sᶜ ≠ ⊤
Tactic:
exact stabilizer_ne_top' (sᶜ) hsc hs'
Proof state after:
no goals
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
intro a ha b hb
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
by_cases hab : a = b
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
use 1
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
⊢ 1 ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧ 1 • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a = b
⊢ 1 ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧ 1 • a = b
Tactic:
simp only [hab, Subgroup.one_mem, one_smul, eq_self_iff_true, and_self_iff]
Proof state after:
no goals
Theorem: alternatingGroup.moves_in
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
rw [← Ne.def] at hab
Proof state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
cases' le_or_gt (Set.ncard t) 2 with ht ht'
Proof state after:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b

case neg.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht' : Set.ncard t > 2
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
have h : 1 < Set.ncard (tᶜ : Set α) := by
  by_contra h
  rw [not_lt] at h
  rw [← not_lt] at hα
  apply hα
  rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl t]
  apply Nat.lt_succ_of_le
  apply add_le_add ht h
Proof state after:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : 1 < Set.ncard tᶜ
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : 1 < Set.ncard tᶜ
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
rw [Set.one_lt_ncard_iff] at h
Proof state after:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : ∃ a b, a ∈ tᶜ ∧ b ∈ tᶜ ∧ a ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : ∃ a b, a ∈ tᶜ ∧ b ∈ tᶜ ∧ a ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
obtain ⟨c, d, hc, hd, hcd⟩ := h
Proof state after:
case neg.inl.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg.inl.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
simp only [Ne.def] at hcd
Proof state after:
case neg.inl.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case neg.inl.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
use Equiv.swap a b * Equiv.swap c d
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧
    (Equiv.swap a b * Equiv.swap c d) • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧
    (Equiv.swap a b * Equiv.swap c d) • a = b
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ (Equiv.swap a b * Equiv.swap c d) • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
⊢ 1 < Set.ncard tᶜ
Tactic:
by_contra h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : ¬1 < Set.ncard tᶜ
⊢ False
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : ¬1 < Set.ncard tᶜ
⊢ False
Tactic:
rw [not_lt] at h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ False
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ False
Tactic:
rw [← not_lt] at hα
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : ¬Fintype.card α < 4
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ False
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : ¬Fintype.card α < 4
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ False
Tactic:
apply hα
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : ¬Fintype.card α < 4
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ Fintype.card α < 4
Theorem: alternatingGroup.moves_in
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : ¬Fintype.card α < 4
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ Fintype.card α < 4
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl t]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : ¬Fintype.card α < 4
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht : Set.ncard t ≤ 2
h : Set.ncard tᶜ ≤ 1
⊢ Set.ncard t + Set.ncard tᶜ < 4