internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.moves_in
Proof state before:
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
ht : t ⊆ {a, b}
⊢ False
Tactic:
apply ht'
Proof state after:
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
ht : t ⊆ {a, b}
⊢ Set.ncard t ≤ 2
Theorem: alternatingGroup.moves_in
Proof state before:
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
ht : t ⊆ {a, b}
⊢ Set.ncard t ≤ 2
Tactic:
convert Set.ncard_le_ncard ht
Proof state after:
case h.e'_4
α : 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
ht : t ⊆ {a, b}
⊢ 2 = Set.ncard {a, b}
Theorem: alternatingGroup.moves_in
Proof state before:
case h.e'_4
α : 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
ht : t ⊆ {a, b}
⊢ 2 = Set.ncard {a, b}
Tactic:
rw [(Set.ncard_pair hab).symm]
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 : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht' : Set.ncard t > 2
this : ∃ c ∈ t, c ≠ a ∧ c ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
obtain ⟨c, hc, hca, hcb⟩ := this
Proof state after:
case 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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
case 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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ ∃ g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α, g • a = b
Tactic:
use Equiv.swap a c * Equiv.swap a b
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧
    (Equiv.swap a c * Equiv.swap a b) • 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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ∧
    (Equiv.swap a c * Equiv.swap a b) • 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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ 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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c * Equiv.swap a b) • a = b
Theorem: alternatingGroup.moves_in
Proof state before:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
Tactic:
simp only [Subgroup.mem_inf]
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t ∧ Equiv.swap a c * Equiv.swap a b ∈ alternatingGroup α
Theorem: alternatingGroup.moves_in
Proof state before:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t ∧ Equiv.swap a c * Equiv.swap a b ∈ alternatingGroup α
Tactic:
constructor
Proof state after:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t

case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ alternatingGroup α
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ stabilizer (Equiv.Perm α) t
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le _ _ t.toFinite]
Proof state after:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c * Equiv.swap a b) • t ⊆ t
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c * Equiv.swap a b) • t ⊆ t
Tactic:
rintro _ ⟨x, hx, rfl⟩
Proof state after:
case h.left.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
⊢ (fun x => (Equiv.swap a c * Equiv.swap a b) • x) x ∈ t
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
⊢ (fun x => (Equiv.swap a c * Equiv.swap a b) • x) x ∈ t
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
case h.left.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
by_cases hxa : x = a
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t

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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : ¬x = a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
rw [hxa, Equiv.swap_apply_left]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ (Equiv.swap a c) b ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ (Equiv.swap a c) b ∈ t
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hab.symm hcb.symm]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ b ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x = a
⊢ b ∈ t
Tactic:
exact hb
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : ¬x = a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
rw [← Ne.def] at hxa
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
by_cases hxb : x = 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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x = b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t

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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : ¬x = b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x = b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
rw [hxb, Equiv.swap_apply_right, Equiv.swap_apply_left]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x = b
⊢ c ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x = b
⊢ c ∈ t
Tactic:
exact hc
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : ¬x = b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
rw [← Ne.def] at hxb
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
⊢ (Equiv.swap a c) ((Equiv.swap a b) x) ∈ t
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hxa hxb]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
⊢ (Equiv.swap a c) x ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
⊢ (Equiv.swap a c) x ∈ t
Tactic:
by_cases hxc : x = c
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x = c
⊢ (Equiv.swap a c) x ∈ t

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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : ¬x = c
⊢ (Equiv.swap a c) x ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x = c
⊢ (Equiv.swap a c) x ∈ t
Tactic:
rw [hxc, Equiv.swap_apply_right]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x = c
⊢ a ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x = c
⊢ a ∈ t
Tactic:
exact ha
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : ¬x = c
⊢ (Equiv.swap a c) x ∈ t
Tactic:
rw [← Ne.def] at hxc
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x ≠ c
⊢ (Equiv.swap a c) x ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x ≠ c
⊢ (Equiv.swap a c) x ∈ t
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hxa hxc]
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x ≠ c
⊢ x ∈ t
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
ht' : Set.ncard t > 2
c : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
x : α
hx : x ∈ t
hxa : x ≠ a
hxb : x ≠ b
hxc : x ≠ c
⊢ x ∈ t
Tactic:
exact hx
Proof state after:
no goals
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.swap a c * Equiv.swap a b ∈ alternatingGroup α
Tactic:
simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul]
Proof state after:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.Perm.sign (Equiv.swap a c) * Equiv.Perm.sign (Equiv.swap a b) = 1
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.Perm.sign (Equiv.swap a c) * Equiv.Perm.sign (Equiv.swap a b) = 1
Tactic:
rw [Equiv.Perm.sign_swap hab]
Proof state after:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.Perm.sign (Equiv.swap a c) * -1 = 1
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ Equiv.Perm.sign (Equiv.swap a c) * -1 = 1
Tactic:
rw [Equiv.Perm.sign_swap (Ne.symm hca)]
Proof state after:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ -1 * -1 = 1
Theorem: alternatingGroup.moves_in
Proof state before:
case h.left.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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ -1 * -1 = 1
Tactic:
simp only [Int.units_mul_self]
Proof state after:
no goals
Theorem: alternatingGroup.moves_in
Proof state before:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c * Equiv.swap a b) • a = b
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c) ((Equiv.swap a b) a) = b
Theorem: alternatingGroup.moves_in
Proof state before:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c) ((Equiv.swap a b) a) = b
Tactic:
rw [Equiv.swap_apply_left]
Proof state after:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c) b = b
Theorem: alternatingGroup.moves_in
Proof state before:
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 : α
hc : c ∈ t
hca : c ≠ a
hcb : c ≠ b
⊢ (Equiv.swap a c) b = b
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (Ne.symm hab) (Ne.symm hcb)]
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 : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
ht' : Set.ncard t > 2
this : Set.Nonempty (t \ {a, b})
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Tactic:
obtain ⟨c, h⟩ := this
Proof state after:
case 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 : α
h : c ∈ t \ {a, b}
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Theorem: alternatingGroup.moves_in
Proof state before:
case 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 : α
h : c ∈ t \ {a, b}
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Tactic:
simp only [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, not_or] at h
Proof state after:
case 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 : α
h : c ∈ t ∧ ¬c = a ∧ ¬c = b
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Theorem: alternatingGroup.moves_in
Proof state before:
case 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 : α
h : c ∈ t ∧ ¬c = a ∧ ¬c = b
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Tactic:
use c
Proof state after:
no goals
Theorem: alternatingGroup.moves_in'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g, g • a = b
Tactic:
intro a ha b hb
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Theorem: alternatingGroup.moves_in'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Tactic:
obtain ⟨g, hg, H⟩ := moves_in hα t a ha b hb
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b