Theorem: alternatingGroup.center_bot (Jordan/V4.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) = ⊥
Tactic:
rw [eq_bot_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) ≤ ⊥

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) ≤ ⊥
Tactic:
rintro ⟨g, hg⟩ hg'
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } ∈ ⊥
Tactic:
simp only [Subgroup.mem_bot]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } = 1

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } = 1
Tactic:
simp only [← Subtype.coe_inj, Subgroup.coe_mk, Subgroup.coe_one]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ g = 1

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ g = 1
Tactic:
rw [← Equiv.Perm.support_eq_empty_iff]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ Equiv.Perm.support g = ∅

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ Equiv.Perm.support g = ∅
Tactic:
rw [Finset.eq_empty_iff_forall_not_mem]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ ∀ (x : α), x ∉ Equiv.Perm.support g

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ ∀ (x : α), x ∉ Equiv.Perm.support g
Tactic:
intro a ha
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
⊢ False

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
⊢ False
Tactic:
let b := g a
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ False

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ False
Tactic:
have hab : b ≠ a := by simp only [b]; rw [← Equiv.Perm.mem_support]; exact ha
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ False

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ False
Tactic:
have : ({a, b} : Finset α)ᶜ.Nonempty :=
  by
  rw [← Finset.card_compl_lt_iff_nonempty, compl_compl, Finset.card_pair hab.symm]
  refine' lt_of_lt_of_le (by norm_num) hα4
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
this : {a, b}ᶜ.Nonempty
⊢ False

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
this : {a, b}ᶜ.Nonempty
⊢ False
Tactic:
obtain ⟨c, hc⟩ := this
State after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : c ∈ {a, b}ᶜ
⊢ False

State before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : c ∈ {a, b}ᶜ
⊢ False
Tactic:
simp only [Finset.compl_insert, Finset.mem_erase, Ne.def, Finset.mem_compl,
  Finset.mem_singleton] at hc
State after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ False

State before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ False
Tactic:
have h2trans : MulAction.IsMultiplyPretransitive (alternatingGroup α) α 2 := by
  refine' MulAction.isMultiplyPretransitive_of_higher (alternatingGroup α) α
    (MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two α) _ _
  exact Nat.le_sub_of_add_le hα4
  simp
State after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
⊢ False

State before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
⊢ False
Tactic:
rw [MulAction.is_two_pretransitive_iff] at h2trans
State after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ False

State before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ False
Tactic:
obtain ⟨k, hk, hk'⟩ := h2trans a b a c hab.symm (Ne.symm hc.left)
State after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ False

State before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ False
Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a ≠ c by
  apply this; rw [← hk']; rfl
State after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a ≠ c

State before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a ≠ c
Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a = (⟨g, hg⟩ : alternatingGroup α) • k • a by
  rw [this, hk]; exact Ne.symm hc.right
State after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a

State before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
Tactic:
rw [Subgroup.mem_center_iff] at hg'
State after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : ∀ (g_1 : ↥(alternatingGroup α)), g_1 * { val := g, property := hg } = { val := g, property := hg } * g_1
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a

State before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : ∀ (g_1 : ↥(alternatingGroup α)), g_1 * { val := g, property := hg } = { val := g, property := hg } * g_1
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
Tactic:
specialize hg' k
State after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
hg' : k * { val := g, property := hg } = { val := g, property := hg } * k
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a

State before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
hg' : k * { val := g, property := hg } = { val := g, property := hg } * k
⊢ k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
Tactic:
simp only [smul_smul, hg']
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ b ≠ a
Tactic:
simp only [b]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ g a ≠ a

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ g a ≠ a
Tactic:
rw [← Equiv.Perm.mem_support]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ a ∈ Equiv.Perm.support g

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ a ∈ Equiv.Perm.support g
Tactic:
exact ha
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ {a, b}ᶜ.Nonempty
Tactic:
rw [← Finset.card_compl_lt_iff_nonempty, compl_compl, Finset.card_pair hab.symm]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ 2 < Fintype.card α

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ 2 < Fintype.card α
Tactic:
refine' lt_of_lt_of_le (by norm_num) hα4
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ 2 < 4
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
Tactic:
refine' MulAction.isMultiplyPretransitive_of_higher (alternatingGroup α) α
  (MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two α) _ _
State after:
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ 2 ≤ Fintype.card α - 2

case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α

State before:
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ 2 ≤ Fintype.card α - 2

case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
exact Nat.le_sub_of_add_le hα4
State after:
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α

State before:
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a ≠ c
⊢ False
Tactic:
apply this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a ≠ c
⊢ k • { val := g, property := hg } • a = c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a ≠ c
⊢ k • { val := g, property := hg } • a = c
Tactic:
rw [← hk']
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a ≠ c
⊢ k • { val := g, property := hg } • a = k • b

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a ≠ c
⊢ k • { val := g, property := hg } • a = k • b
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
⊢ k • { val := g, property := hg } • a ≠ c
Tactic:
rw [this, hk]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
⊢ { val := g, property := hg } • a ≠ c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
this : k • { val := g, property := hg } • a = { val := g, property := hg } • k • a
⊢ { val := g, property := hg } • a ≠ c
Tactic:
exact Ne.symm hc.right
State after:
no goals