awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g

Tactic:
exact hg.mem_commutatorSet_alternatingGroup h5

Premises used: Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
simp :
  ∀ (x x_1 x_2 : Perm α) (h : ⁅x_1, x_2⁆ = x),
    Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x : ℤˣ) (1 : ℤˣ)
⊢ _root_.commutator (Perm α) ≤ alternatingGroup α

Tactic:
simp only [commutator_eq_closure, closure_le, Set.subset_def, mem_commutatorSet_iff,
    SetLike.mem_coe, mem_alternatingGroup, forall_exists_index]

Premises used: Set.subset_def, commutator_eq_closure, Subgroup.closure_le, forall_exists_index, mem_commutatorSet_iff, Equiv.Perm.mem_alternatingGroup, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p q : Perm α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) ⁅p, q⁆ : ℤˣ) (1 : ℤˣ)

Tactic:
simp [map_commutatorElement, commutatorElement_eq_one_iff_commute, Commute.all]

Premises used: commutatorElement_eq_one_iff_commute, map_commutatorElement, Commute.all
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
this :
  Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
rw :
  {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle} ⊆
    (↑(_root_.commutator ↥(alternatingGroup α)) : Set ↥(alternatingGroup α))
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (_root_.commutator ↥(alternatingGroup α)) ⊤

Tactic:
rw [eq_top_iff, ← this, Subgroup.closure_le]

Premises used: eq_top_iff, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
this :
  Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
b : ↥(alternatingGroup α)
hb : Membership.mem (γ := Set ↥(alternatingGroup α)) {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle} b
⊢ b ∈ (↑(_root_.commutator ↥(alternatingGroup α)) : Set ↥(alternatingGroup α))

Tactic:
hb.mem_commutator_alternatingGroup h5

Premises used: Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
this :
  Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
b : ↥(alternatingGroup α)
hb : Membership.mem (γ := Set ↥(alternatingGroup α)) {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle} b
⊢ b ∈ (↑(_root_.commutator ↥(alternatingGroup α)) : Set ↥(alternatingGroup α))

Tactic:
exact hb.mem_commutator_alternatingGroup h5

Premises used: Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
suffices :
  Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (_root_.commutator ↥(alternatingGroup α)) ⊤

Tactic:
suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤ by
    rw [eq_top_iff, ← this, Subgroup.closure_le]
    intro b hb
    exact hb.mem_commutator_alternatingGroup h5
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw :
  Eq.{u_1 + 1} (α := Subgroup ↥(closure {σ : Perm α | σ.IsThreeCycle}))
    (closure {b : ↥(closure {σ : Perm α | σ.IsThreeCycle}) | (↑b : Perm α).IsThreeCycle}) ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤

Tactic:
rw [← closure_three_cycles_eq_alternating]

Premises used: Equiv.Perm.closure_three_cycles_eq_alternating
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(closure {σ : Perm α | σ.IsThreeCycle}))
    (closure {b : ↥(closure {σ : Perm α | σ.IsThreeCycle}) | (↑b : Perm α).IsThreeCycle}) ⊤

Tactic:
Subgroup.closure_closure_coe_preimage

Premises used: Set.Mem, setOf, Subgroup.closure_closure_coe_preimage, Set.preimage, Equiv.Perm.IsThreeCycle
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(closure {σ : Perm α | σ.IsThreeCycle}))
    (closure {b : ↥(closure {σ : Perm α | σ.IsThreeCycle}) | (↑b : Perm α).IsThreeCycle}) ⊤

Tactic:
exact Subgroup.closure_closure_coe_preimage

Premises used: Subgroup.closure_closure_coe_preimage
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw : Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
rw₁ : Subgroup.map (alternatingGroup α).subtype ⊤ = alternatingGroup α
rw₂ : (alternatingGroup α).subtype.range = alternatingGroup α
rw₃ rw₄ : alternatingGroup α = alternatingGroup α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α

Tactic:
rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]

Premises used: MonoidHom.range_eq_map, commutator_alternatingGroup_eq_top, Subgroup.range_subtype, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
apply : alternatingGroup α ≤ _root_.commutator (Perm α)
⊢ _root_.commutator (Perm α) = alternatingGroup α

Tactic:
apply le_antisymm alternatingGroup.commutator_perm_le

Premises used: le_antisymm, alternatingGroup.commutator_perm_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw : ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)

Tactic:
rw [← commutator_alternatingGroup_eq_self h5]

Premises used: commutator_alternatingGroup_eq_self
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)

Tactic:
commutator_mono le_top le_top

Premises used: Subgroup.commutator_mono, Set.Mem, le_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)

Tactic:
exact commutator_mono le_top le_top

Premises used: Subgroup.commutator_mono, le_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
rw :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1) {n : ℕ}
    (hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
rw [mem_alternatingGroup, sign_of_cycleType] at hg0

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
rw : g.support.card ≤ Fintype.card α
⊢ g.cycleType.sum ≤ 4

Tactic:
rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]

Premises used: Equiv.Perm.sum_cycleType, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.support.card ≤ Fintype.card α

Tactic:
g.support.card_le_univ

Premises used: Equiv.Perm.support, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.support.card ≤ Fintype.card α

Tactic:
exact g.support.card_le_univ

Premises used: Equiv.Perm.support, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.cycleType.sum ≤ 4

Tactic:
have h1 : g.cycleType.sum ≤ 4 := by
    rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
    exact g.support.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
⊢ k ≤ 4

Tactic:
have hk4 := (Multiset.le_sum_of_mem hk).trans h1
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
⊢ 1 < k

Tactic:
have hk1 := one_lt_of_mem_cycleType hk
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
hk1 : 1 < k
2 : ∀ (hk : 2 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 2 4) (hk1 : LT.lt (α := ℕ) 1 2), Eq (α := ℕ) 2 2
3 : ∀ (hk : 3 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 3 4) (hk1 : LT.lt (α := ℕ) 1 3), Eq (α := ℕ) 3 2
4 : ∀ (hk : 4 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 4 4) (hk1 : LT.lt (α := ℕ) 1 4), Eq (α := ℕ) 4 2
⊢ k = 2

Tactic:
interval_cases k
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 2 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 2 4
hk1 : LT.lt (α := ℕ) 1 2
⊢ Eq (α := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 3 4
hk1 : LT.lt (α := ℕ) 1 3
3 :
  ∀ (hg : ∀ b ∈ g.cycleType, b ∣ HPow.hPow (α := ℕ) 2 n) (h1 : g.cycleType.sum ≤ 4) (k : ℕ) (hk : 3 ∈ g.cycleType)
    (hk4 : LE.le (α := ℕ) 3 4) (hk1 : LT.lt (α := ℕ) 1 3), Eq (α := ℕ) 3 2
⊢ Eq (α := ℕ) 3 2

Tactic:
rw [← lcm_cycleType, Multiset.lcm_dvd] at hg

Premises used: Equiv.Perm.lcm_cycleType, Multiset.lcm_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : ∀ b ∈ g.cycleType, b ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 3 4
hk1 : LT.lt (α := ℕ) 1 3
⊢ Eq (α := ℕ) 3 2

Tactic:
Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)

Premises used: Nat.prime_eq_prime_of_dvd_pow, Nat.prime_two, Nat.prime_three, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : ∀ b ∈ g.cycleType, b ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 3 4
hk1 : LT.lt (α := ℕ) 1 3
⊢ Eq (α := ℕ) 3 2

Tactic:
exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)

Premises used: Nat.prime_eq_prime_of_dvd_pow, Nat.prime_two, Nat.prime_three, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
4 : ∀ (hg0 : Ne (α := ℕ) 4 2), HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
⊢ Eq (α := ℕ) 4 2

Tactic:
contrapose! hg0
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
4 : ∀ (t : Multiset ℕ) (ht : g.cycleType = 4 ::ₘ t), HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1

Tactic:
obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk

Premises used: Multiset.exists_cons_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
ht : g.cycleType = 4 ::ₘ t
⊢ t = Multiset.replicate t.card 0

Tactic:
rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1

Premises used: le_zero_iff, add_le_iff_nonpos_right, Multiset.sum_cons, Multiset.eq_replicate_card, Multiset.sum_eq_zero_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
ht : g.cycleType = 4 ::ₘ t
h1₁ : t = Multiset.replicate t.card 0
⊢ g.cycleType = 4 ::ₘ t

Tactic:
rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1

Premises used: le_zero_iff, add_le_iff_nonpos_right, Multiset.sum_cons, Multiset.eq_replicate_card, Multiset.sum_eq_zero_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
⊢ 0 ∉ g.cycleType

Tactic:
have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ t = 0

Tactic:
simpa [h1 ▸ ht, Multiset.mem_replicate] using h

Premises used: Multiset.mem_replicate
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ t = 0

Tactic:
replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : t = 0
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1

Tactic:
simp [ht, h, Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
⊢ ∀ k ∈ g.cycleType, k = 2

Tactic:
have h2 : ∀ k ∈ g.cycleType, k = 2 := by
    intro k hk
    have hk4 := (Multiset.le_sum_of_mem hk).trans h1
    have hk1 := one_lt_of_mem_cycleType hk
    interval_cases k
    · rfl
    · rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
      exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)
    · contrapose! hg0
      obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk
      rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1
      have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
      replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
      simp [ht, h, Units.ext_iff]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
h2 : ∀ k ∈ g.cycleType, k = 2
⊢ g.cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
rw [← Multiset.eq_replicate_card] at h2

Premises used: Multiset.eq_replicate_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType.card ≤ 4 / 2

Tactic:
rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1

Premises used: two_pos, Multiset.sum_replicate, Nat.le_div_iff_mul_le, smul_eq_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h1₁ : g.cycleType.card ≤ 4 / 2
⊢ g.cycleType = Multiset.replicate g.cycleType.card 2

Tactic:
rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1

Premises used: two_pos, Multiset.sum_replicate, Nat.le_div_iff_mul_le, smul_eq_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.card ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
0 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 0) = 1) (h1 : 0 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 0 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
1 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 1) = 1) (h1 : 1 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 1 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
2 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 2) = 1) (h1 : 2 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 2 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
interval_cases g.cycleType.card

Premises used: Equiv.Perm.cycleType, Multiset.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 0) = 1
h1 : 0 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 0 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
simp [h2, Units.ext_iff] at hg0 ⊢

Premises used: Units.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 1) = 1
h1 : 1 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 1 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
simp [h2, Units.ext_iff] at hg0 ⊢

Premises used: Units.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 2) = 1
h1 : 2 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 2 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
simp [h2, Units.ext_iff] at hg0 ⊢

Premises used: Units.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
rw : LT.lt (α := ℕ) 1 4
⊢ Nontrivial α

Tactic:
rw [← Finite.one_lt_card_iff_nontrivial, hα4]

Premises used: Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ LT.lt (α := ℕ) 1 4

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Nontrivial α

Tactic:
have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
rw : Nat.factorial 4 / 2 = 12
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 12

Tactic:
rw [nat_card_alternatingGroup, hα4]

Premises used: nat_card_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 / 2 = 12

Tactic:
decide