internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.center_bot
Proof 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
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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'
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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']
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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]
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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]
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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]
Proof 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 α
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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 α) _ _
Proof 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 α
Theorem: alternatingGroup.center_bot
Proof 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
Proof 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 α
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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']
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof 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]
Proof 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
Theorem: alternatingGroup.center_bot
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ V4 α = commutator ↥(alternatingGroup α)
Tactic:
haveI : (V4 α).Normal := V4_is_normal α hα4
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ V4 α = commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
⊢ V4 α = commutator ↥(alternatingGroup α)
Tactic:
have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ := by
  have : Nontrivial (Subgroup (alternatingGroup α)) := by
    rw [Subgroup.nontrivial_iff]
    rw [← Fintype.one_lt_card_iff_nontrivial]
    rw [A4_card α hα4]
    norm_num
  rw [Ne.def, commutator, Subgroup.commutator_eq_bot_iff_le_centralizer,
    ← eq_top_iff, Subgroup.coe_top, Subgroup.centralizer_univ,
    alternatingGroup.center_bot _]
  exact bot_ne_top
  rw [hα4]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
⊢ V4 α = commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
⊢ V4 α = commutator ↥(alternatingGroup α)
Tactic:
obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
⊢ V4 α = commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
have hk2 := comm_le hk
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k ∈ V4 α
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k ∈ V4 α
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
rw [← Subgroup.mem_carrier, V4_carrier_eq α hα4] at hk2
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
cases' hk2 with hk2 hk2
Proof state after:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = 0
⊢ Equiv.Perm.cycleType ↑k = {2, 2}

case intro.intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ commutator ↥(alternatingGroup α) ≤ V4 α
Tactic:
rw [← Subgroup.quotient_isCommutative_iff_commutator_le]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply isCommutative_of_prime_order (hp := Nat.fact_prime_three) _
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card (↥(alternatingGroup α) ⧸ V4 α) = 3
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card (↥(alternatingGroup α) ⧸ V4 α) = 3
Tactic:
apply mul_left_injective₀ _
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ (fun a => a * ?m.92416) (Fintype.card (↥(alternatingGroup α) ⧸ V4 α)) = (fun a => a * ?m.92416) 3

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ℕ

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ?m.92416 ≠ 0
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ (fun a => a * ?m.92416) (Fintype.card (↥(alternatingGroup α) ⧸ V4 α)) = (fun a => a * ?m.92416) 3

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ℕ

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ?m.92416 ≠ 0
Tactic:
dsimp
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card (↥(alternatingGroup α) ⧸ V4 α) * ?m.92416 = 3 * ?m.92416

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ℕ

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ?m.92416 ≠ 0
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card (↥(alternatingGroup α) ⧸ V4 α) * ?m.92416 = 3 * ?m.92416

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ℕ

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ ?m.92416 ≠ 0
Tactic:
rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup, V4_card α hα4, A4_card α hα4]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card ↥(V4 α) ≠ 0
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card ↥(V4 α) ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
⊢ commutator ↥(alternatingGroup α) ≠ ⊥
Tactic:
have : Nontrivial (Subgroup (alternatingGroup α)) := by
  rw [Subgroup.nontrivial_iff]
  rw [← Fintype.one_lt_card_iff_nontrivial]
  rw [A4_card α hα4]
  norm_num
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this✝ : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
this : Nontrivial (Subgroup ↥(alternatingGroup α))
⊢ commutator ↥(alternatingGroup α) ≠ ⊥