internlm/Lean-Github huggingface dataset:
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 α
this : Nontrivial (Subgroup ↥(alternatingGroup α))
⊢ commutator ↥(alternatingGroup α) ≠ ⊥
Tactic:
rw [Ne.def, commutator, Subgroup.commutator_eq_bot_iff_le_centralizer,
  ← eq_top_iff, Subgroup.coe_top, Subgroup.centralizer_univ,
  alternatingGroup.center_bot _]
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 α))
⊢ ¬⊥ = ⊤

α : 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 α))
⊢ 4 ≤ Fintype.card α
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 α
this : Nontrivial (Subgroup ↥(alternatingGroup α))
⊢ ¬⊥ = ⊤

α : 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 α))
⊢ 4 ≤ Fintype.card α
Tactic:
exact bot_ne_top
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 α))
⊢ 4 ≤ Fintype.card α
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 α
this : Nontrivial (Subgroup ↥(alternatingGroup α))
⊢ 4 ≤ Fintype.card α
Tactic:
rw [hα4]
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 α
⊢ Nontrivial (Subgroup ↥(alternatingGroup α))
Tactic:
rw [Subgroup.nontrivial_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
⊢ Nontrivial ↥(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 α
⊢ Nontrivial ↥(alternatingGroup α)
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
⊢ 1 < Fintype.card ↥(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 α
⊢ 1 < Fintype.card ↥(alternatingGroup α)
Tactic:
rw [A4_card α 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 α
⊢ 1 < 12
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 α
⊢ 1 < 12
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 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ V4 α = commutator ↥(alternatingGroup α)
Tactic:
refine' le_antisymm _ comm_le
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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ 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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ V4 α ≤ commutator ↥(alternatingGroup α)
Tactic:
intro g hg
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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g ∈ V4 α
⊢ g ∈ 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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g ∈ V4 α
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
rw [← Subgroup.mem_carrier, V4_carrier_eq α hα4] at hg
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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ∈ 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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
cases' hg with hg hg
Proof state after:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = 0
⊢ g ∈ commutator ↥(alternatingGroup α)

case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = 0
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
rw [Equiv.Perm.cycleType_eq_zero, OneMemClass.coe_eq_one] at hg
Proof state after:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1
⊢ g ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
rw [hg]
Proof state after:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1
⊢ 1 ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1
⊢ 1 ∈ commutator ↥(alternatingGroup α)
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case 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
hk22 : Equiv.Perm.cycleType ↑k = {2, 2}
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
Proof state after:
case 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
g : ↥(alternatingGroup α)
hk22 : ∃ c, c * ↑k * c⁻¹ = ↑g
hg : Equiv.Perm.cycleType ↑g = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case 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
g : ↥(alternatingGroup α)
hk22 : ∃ c, c * ↑k * c⁻¹ = ↑g
hg : Equiv.Perm.cycleType ↑g = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
obtain ⟨c, hc⟩ := hk22
Proof state after:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : c * ↑k * c⁻¹ = ↑g
⊢ g ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : c * ↑k * c⁻¹ = ↑g
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
Proof state after:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
⊢ g ∈ commutator ↥(alternatingGroup α)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
⊢ g ∈ commutator ↥(alternatingGroup α)
Tactic:
simp only [commutator, ← hc]
Proof state after:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Tactic:
let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
Proof state after:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Tactic:
suffices (⊤ : Subgroup (alternatingGroup α)) =
  Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
  rw [this, ← Subgroup.map_commutator]
  refine' Subgroup.mem_map_of_mem _ hk
Proof state after:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
Tactic:
apply symm
Proof state after:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ Subgroup.map (MulEquiv.toMonoidHom fc) ⊤ = ⊤
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ Subgroup.map (MulEquiv.toMonoidHom fc) ⊤ = ⊤
Tactic:
rw [← MonoidHom.range_eq_map]
Proof state after:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ MonoidHom.range (MulEquiv.toMonoidHom fc) = ⊤
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ MonoidHom.range (MulEquiv.toMonoidHom fc) = ⊤
Tactic:
rw [MonoidHom.range_top_iff_surjective]
Proof state after:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom fc)
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case inr.intro.a
α : 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
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom fc)
Tactic:
exact MulEquiv.surjective _
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 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
this : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Tactic:
rw [this, ← Subgroup.map_commutator]
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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
this : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
⊢ (MulAut.conjNormal c) k ∈ Subgroup.map (MulEquiv.toMonoidHom fc) ⁅⊤, ⊤⁆
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 α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : Equiv.Perm.cycleType ↑g = {2, 2}
c : Equiv.Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
this : ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤
⊢ (MulAut.conjNormal c) k ∈ Subgroup.map (MulEquiv.toMonoidHom fc) ⁅⊤, ⊤⁆
Tactic:
refine' Subgroup.mem_map_of_mem _ hk
Proof state after:
no goals
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
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}
Tactic:
exfalso
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
⊢ False