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

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
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ V4 α = commutator ↥(alternatingGroup α)

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

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

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

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

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

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

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) _
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card (↥(alternatingGroup α) ⧸ V4 α) = 3

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

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

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]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
⊢ Fintype.card ↥(V4 α) ≠ 0

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

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
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 α) ≠ ⊥

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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]
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 ∈ ⁅⊤, ⊤⁆

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
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 ∈ ⁅⊤, ⊤⁆

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

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

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

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

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

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]
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) ⁅⊤, ⊤⁆

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

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

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
⊢ False
Tactic:
apply hk'
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
⊢ k = 1

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
⊢ k = 1
Tactic:
rw [Equiv.Perm.cycleType_eq_zero] at hk2
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 : ↑k = 1
⊢ k = 1

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 : ↑k = 1
⊢ k = 1
Tactic:
simp only [← Subtype.coe_inj, hk2, Subgroup.coe_one]
State after:
no goals

State before:
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}
Tactic:
exact hk2
State after:
no goals