internlm/Lean-Github huggingface dataset:
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
⊢ Set.ncard t + Set.ncard tᶜ < 4
Tactic:
apply Nat.lt_succ_of_le
Proof state after:
case a
α : 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ᶜ ≤ 3
Theorem: alternatingGroup.moves_in
Proof state before:
case a
α : 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ᶜ ≤ 3
Tactic:
apply add_le_add ht h
Proof state after:
no goals
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ stabilizer (Equiv.Perm α) t ∧ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ stabilizer (Equiv.Perm α) t ∧ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ (Equiv.swap a b * Equiv.swap c d) • 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ (Equiv.swap a b * Equiv.swap c d) • 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
⊢ (fun x => (Equiv.swap a b * Equiv.swap c d) • 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
⊢ (fun x => (Equiv.swap a b * Equiv.swap c d) • 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
⊢ (Equiv.swap a b) ((Equiv.swap c d) 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
⊢ (Equiv.swap a b) ((Equiv.swap c d) x) ∈ t
Tactic:
have hx_ne : ∀ u ∈ tᶜ, x ≠ u := fun u hu h => Set.mem_compl hu (by rw [← h]; exact hx)
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
⊢ (Equiv.swap a b) ((Equiv.swap c d) 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
⊢ (Equiv.swap a b) ((Equiv.swap c d) x) ∈ t
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (hx_ne c hc) (hx_ne d hd)]
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : x = a
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
⊢ (Equiv.swap a b) x ∈ t
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
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
u : α
hu : u ∈ tᶜ
h : x = u
⊢ u ∈ t
Tactic:
rw [← 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
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
u : α
hu : u ∈ tᶜ
h : x = u
⊢ x ∈ t
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
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
u : α
hu : u ∈ tᶜ
h : x = u
⊢ x ∈ t
Tactic:
exact hx
Proof state after:
no goals
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : x = a
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : x = b
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : ¬x = b
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : x = b
⊢ (Equiv.swap a b) x ∈ t
Tactic:
rw [hxb, 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : x = b
⊢ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : x = b
⊢ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : ¬x = b
⊢ (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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : ¬x = 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
x : α
hx : x ∈ t
hx_ne : ∀ u ∈ tᶜ, x ≠ u
hxa : ¬x = a
hxb : ¬x = b
⊢ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.swap a b * Equiv.swap c d ∈ 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.Perm.sign (Equiv.swap a b) * Equiv.Perm.sign (Equiv.swap c d) = 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ Equiv.Perm.sign (Equiv.swap a b) * Equiv.Perm.sign (Equiv.swap c d) = 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ -1 * Equiv.Perm.sign (Equiv.swap c d) = 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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ -1 * Equiv.Perm.sign (Equiv.swap c d) = 1
Tactic:
rw [Equiv.Perm.sign_swap hcd]
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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ -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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ -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 d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : ¬c = d
⊢ (Equiv.swap a b * Equiv.swap c d) • 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 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:
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
Tactic:
rw [Set.mem_compl_iff t] at hc hd
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 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:
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
Tactic:
have hac : a ≠ c := by intro h; apply hc; rw [← h]; exact ha
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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
⊢ (Equiv.swap a b) ((Equiv.swap c d) 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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
⊢ (Equiv.swap a b) ((Equiv.swap c d) a) = b
Tactic:
have had : a ≠ d := by intro h; apply hd; rw [← h]; exact ha
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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
had : a ≠ d
⊢ (Equiv.swap a b) ((Equiv.swap c d) 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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
had : a ≠ d
⊢ (Equiv.swap a b) ((Equiv.swap c d) a) = b
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hac had]
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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
had : a ≠ d
⊢ (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 d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
had : a ≠ d
⊢ (Equiv.swap a b) a = b
Tactic:
rw [Equiv.swap_apply_left]
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
⊢ a ≠ c
Tactic:
intro 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ False
Tactic:
apply hc
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ c ∈ t
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ c ∈ t
Tactic:
rw [← 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ a ∈ t
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
h : a = c
⊢ a ∈ t
Tactic:
exact ha
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
⊢ a ≠ d
Tactic:
intro 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ False
Tactic:
apply hd
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ d ∈ t
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ d ∈ t
Tactic:
rw [← 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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ a ∈ t
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
c d : α
hc : c ∉ t
hd : d ∉ t
hcd : ¬c = d
hac : a ≠ c
h : a = d
⊢ a ∈ t
Tactic:
exact ha
Proof state after:
no goals
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
⊢ ∃ c ∈ t, c ≠ a ∧ c ≠ b
Tactic:
suffices (t \ {a, b}).Nonempty by
  obtain ⟨c, h⟩ := this
  simp only [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, not_or] at h
  use c
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
⊢ Set.Nonempty (t \ {a, b})
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
⊢ Set.Nonempty (t \ {a, b})
Tactic:
rw [Set.nonempty_diff]
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
⊢ ¬t ⊆ {a, b}
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
⊢ ¬t ⊆ {a, b}
Tactic:
intro 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}
⊢ False
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:
rw [gt_iff_lt, ← not_le] at 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}
⊢ False