Theorem: alternatingGroup.moves_in (Jordan/AlternatingMaximal.lean)

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
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

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
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

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
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

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]
State after:
no goals

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
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

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'
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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α
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

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α
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

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]
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

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
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

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
State after:
no goals

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]
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 α

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
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 α

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]
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

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⟩
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

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]
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

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)
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

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)]
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

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
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

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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

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]
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

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]
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

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]
State after:
no goals

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]
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

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
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

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
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

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
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

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]
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

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]
State after:
no goals

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
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

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
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

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]
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

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
State after:
no goals

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
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

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
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

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]
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

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
State after:
no goals

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
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})

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]
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}

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
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

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'
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

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'
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

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
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}

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]
State after:
no goals

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
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

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
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

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
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

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]
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 α

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
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 α

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]
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

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⟩
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

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]
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

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
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

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]
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

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]
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

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
State after:
no goals

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
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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]
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

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]
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

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)]
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

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]
State after:
no goals

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]
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

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]
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

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)]
State after:
no goals

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
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

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
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

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
State after:
no goals