awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
hNX :
  Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 3) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 3) : Type u_1))
    Set.univ
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N

Tactic:
apply iwasawaStructure_three.commutator_le

Premises used: MulAction.IwasawaStructure.commutator_le, alternatingGroup.iwasawaStructure_three
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
⊢ LT.lt (α := ℕ) 0 3

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
⊢ 3 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
⊢ Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 3) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 3) : Type u_1))
    Set.univ

Tactic:
exact fixedPoints_ne_univ_of_faithfulSMul (by norm_num) (by grind)

Premises used: Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
k : ↥(alternatingGroup α)
⊢ Nat.card.{u_1} ↥s = 4

Tactic:
simpa
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
k : ↥(alternatingGroup α)
⊢ Nat.card.{u_1} ↥s = 4

Tactic:
have hs : Nat.card s = 4 := by simpa
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
pos :
  ∀ (hk : (↑k : Perm α).support ⊆ s),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
      (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
neg :
  ∀ (hk : ¬(↑k : Perm α).support ⊆ s),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
      (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})

Tactic:
by_cases hk : (k : Perm α).support ⊆ s

Premises used: Equiv.Perm.support, Subtype.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
hk : (↑k : Perm α).support ⊆ s
pos :
  ∀ (σ : ↥(alternatingGroup ↥s))
    (hk : support (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) ⊆ s),
    Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
        (Subgroup.map (ofSubtype s) (kleinFour ↥s))
        ((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ : ↥(alternatingGroup α)) ↔
      support (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) ⊆ s ∧
        (Eq.{u_1 + 1} (α := Perm α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α)
            1 ∨
          cycleType.{u_1} (α := α)
              (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) =
            {2, 2})
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})

Tactic:
obtain ⟨σ, rfl⟩ := (mem_range_ofSubtype_iff s k).mpr hk

Premises used: Iff.mpr, alternatingGroup.mem_range_ofSubtype_iff, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
hs : Nat.card.{u_1} ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : support (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) ⊆ s
pos :
  Membership.mem (γ := Set ↥(alternatingGroup ↥s))
      ({1} ∪ {g : ↥(alternatingGroup ↥s) | (↑g : Perm ↥s).cycleType = {2, 2}}) σ ↔
    Eq.{u_1 + 1} (α := Perm α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) 1 ∨
      cycleType.{u_1} (α := α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) =
        {2, 2}
⊢ Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
      (Subgroup.map (ofSubtype s) (kleinFour ↥s))
      ((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ : ↥(alternatingGroup α)) ↔
    support (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) ⊆ s ∧
      (Eq.{u_1 + 1} (α := Perm α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α)
          1 ∨
        cycleType.{u_1} (α := α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) =
          {2, 2})

Tactic:
simp_rw [and_iff_right hk, Subgroup.mem_map, ofSubtype_inj, existsAndEq, and_true,
      ← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hs]

Premises used: and_true, ExistsAndEq.existsAndEq, alternatingGroup.coe_kleinFour_of_card_eq_four, and_iff_right, SetLike.mem_coe, alternatingGroup.ofSubtype_inj, Subgroup.mem_map
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
hs : Nat.card.{u_1} ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : support (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) ⊆ s
⊢ Membership.mem (γ := Set ↥(alternatingGroup ↥s))
      ({1} ∪ {g : ↥(alternatingGroup ↥s) | (↑g : Perm ↥s).cycleType = {2, 2}}) σ ↔
    Eq.{u_1 + 1} (α := Perm α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) 1 ∨
      cycleType.{u_1} (α := α) (↑((ofSubtype s : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)) σ) : Perm α) =
        {2, 2}

Tactic:
simp [cycleType_ofSubtype, coe_ofSubtype, map_eq_one_iff _ Perm.ofSubtype_injective]

Premises used: Equiv.Perm.cycleType_ofSubtype, alternatingGroup.coe_ofSubtype, map_eq_one_iff, Equiv.Perm.ofSubtype_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
hk : ¬(↑k : Perm α).support ⊆ s
neg : k ∉ Subgroup.map (ofSubtype s) (kleinFour ↥s)
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})

Tactic:
simp_rw [hk, false_and, iff_false]

Premises used: iff_false, false_and
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
hk : ¬(↑k : Perm α).support ⊆ s
neg :
  ∀ (hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k),
    (↑k : Perm α).support ⊆ s
⊢ k ∉ Subgroup.map (ofSubtype s) (kleinFour ↥s)

Tactic:
contrapose! hk
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k
⊢ (↑k : Perm α).support ⊆ s

Tactic:
(mem_range_ofSubtype_iff s k).mp (Subgroup.map_le_range _ _ hk)

Premises used: Subgroup.map_le_range, alternatingGroup.mem_range_ofSubtype_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs_1 : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card.{u_1} ↥s = 4
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k
⊢ (↑k : Perm α).support ⊆ s

Tactic:
exact (mem_range_ofSubtype_iff s k).mp (Subgroup.map_le_range _ _ hk)

Premises used: Subgroup.map_le_range, alternatingGroup.mem_range_ofSubtype_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
g : ↥(alternatingGroup α)
rcases :
  ∀ (g : Perm α) (hg : g ∈ alternatingGroup α),
    Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
        (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)) =
      HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
        ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
          MulAut ↥(alternatingGroup α))
        (Subgroup.map (ofSubtype s) (kleinFour ↥s))
⊢ Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)) =
    HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
      ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
      (Subgroup.map (ofSubtype s) (kleinFour ↥s))

Tactic:
rcases g with ⟨g, hg⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
h :
  ∀ (k : Perm α) (hk : k ∈ alternatingGroup α),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α))
        (Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
          (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)))
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk) ↔
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk ∈
        HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
          ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
              (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
            MulAut ↥(alternatingGroup α))
          (Subgroup.map (ofSubtype s) (kleinFour ↥s))
⊢ Subgroup.map (ofSubtype (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s))
      (kleinFour ↥(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • s)) =
    HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
      ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) :
        MulAut ↥(alternatingGroup α))
      (Subgroup.map (ofSubtype s) (kleinFour ↥s))

Tactic:
ext ⟨k, hk⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ (g • s).card = 4

Tactic:
simpa
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
s : (↑(Set.powersetCard α 4) : Type u_1)
⊢ Nat.card.{u_1} ↥(↑s : Finset α) = 4

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
s : (↑(Set.powersetCard α 4) : Type u_1)
⊢ IsMulCommutative.{u_1} ↥(kleinFour ↥(↑s : Finset α))

Tactic:
have : IsMulCommutative (kleinFour s) :=
      (kleinFour_isKleinFour (by simp)).isMulCommutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
s : (↑(Set.powersetCard α 4) : Type u_1)
this : IsMulCommutative.{u_1} ↥(kleinFour ↥(↑s : Finset α))
⊢ IsMulCommutative.{u_1} ↥(Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α)))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
rw :
  {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}} ⊆
    (↑(⨆ (s : (↑(Set.powersetCard α 4) : Type u_1)),
          Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α))) :
      Set ↥(alternatingGroup α))
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (⨆ (s : (↑(Set.powersetCard α 4) : Type u_1)),
      Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α)))
    ⊤

Tactic:
rw [eq_top_iff, ← closure_cycleType_eq_two_two_eq_top h5, Subgroup.closure_le]

Premises used: eq_top_iff, Subgroup.closure_le, alternatingGroup.closure_cycleType_eq_two_two_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ (↑g : Perm α).support ∈ Set.powersetCard α 4

Tactic:
simp [← sum_cycleType, hg]

Premises used: Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
apply :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (Subgroup.map
      (ofSubtype
        (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α))
      (kleinFour
        ↥(↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α)))
    g
⊢ g ∈
    (↑(⨆ (s : (↑(Set.powersetCard α 4) : Type u_1)),
          Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α))) :
      Set ↥(alternatingGroup α))

Tactic:
apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, by simp [← sum_cycleType, hg]⟩

Premises used: Subgroup.mem_iSup_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
rw :
  (↑g : Perm α).support ⊆
      (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α) ∧
    ((↑g : Perm α) = 1 ∨ (↑g : Perm α).cycleType = {2, 2})
hs : (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α).card = 4
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (Subgroup.map
      (ofSubtype
        (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α))
      (kleinFour
        ↥(↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α)))
    g

Tactic:
rw [mem_map_kleinFour_ofSubtype]

Premises used: alternatingGroup.mem_map_kleinFour_ofSubtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ (↑g : Perm α).support ⊆
      (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α) ∧
    ((↑g : Perm α) = 1 ∨ (↑g : Perm α).cycleType = {2, 2})

Tactic:
simp [hg, ← sum_cycleType]

Premises used: Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support ⋯) : Finset α).card = 4

Tactic:
simp [hg, ← sum_cycleType]

Premises used: Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
rw : Nontrivial.{u_1} ↥N → N = ⊤
⊢ N = ⊥ ∨ N = ⊤

Tactic:
rw [or_iff_not_imp_left, ← ne_eq, ← Subgroup.nontrivial_iff_ne_bot]

Premises used: ne_eq, Classical.or_iff_not_imp_left, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ LE.le (α := ℕ) 3 4

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
hn : 4 < Nat.card α
hα₁ : Nat.card α ≠ HMul.hMul (α := ℕ) 2 4
⊢ IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)

Tactic:
apply Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num)

Premises used: Set.powersetCard.isPreprimitive_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ 4 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ Nat.card α ≠ HMul.hMul (α := ℕ) 2 4

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)

Tactic:
have : IsPreprimitive (alternatingGroup α) (Set.powersetCard α 4) := by
    apply Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num) <;> grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)
rw : _root_.commutator ↥(alternatingGroup α) ≤ N
⊢ N = ⊤

Tactic:
rw [eq_top_iff, ← commutator_alternatingGroup_eq_top hα]

Premises used: eq_top_iff, commutator_alternatingGroup_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)
hNX :
  Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 4) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 4) : Type u_1))
    Set.univ
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N

Tactic:
apply (iwasawaStructure_four hα).commutator_le

Premises used: MulAction.IwasawaStructure.commutator_le, alternatingGroup.iwasawaStructure_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)
⊢ LT.lt (α := ℕ) 0 4

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)
⊢ 4 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 4) : Type u_1)
⊢ Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 4) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 4) : Type u_1))
    Set.univ

Tactic:
exact fixedPoints_ne_univ_of_faithfulSMul (by norm_num) (by grind)

Premises used: Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
pos : ∀ (hα' : Nat.card α = 6), N = ⊥ ∨ N = ⊤
neg : ∀ (hα' : ¬Nat.card α = 6), N = ⊥ ∨ N = ⊤
⊢ N = ⊥ ∨ N = ⊤

Tactic:
by_cases hα' : Nat.card α = 6

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hα' : Nat.card α = 6
⊢ Nat.card α ≠ 8

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hα' : Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤

Tactic:
apply normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight hα (by grind)

Premises used: alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hα' : ¬Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤

Tactic:
apply normal_subgroup_eq_bot_or_eq_top_of_card_ne_six hα hα'

Premises used: alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_six
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
rw : Nontrivial.{u_1} ↥(alternatingGroup α)
⊢ ∃ (x : ↥(alternatingGroup α)) (y : ↥(alternatingGroup α)), x ≠ y

Tactic:
rw [← _root_.nontrivial_iff]

Premises used: nontrivial_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
nontrivial_of_three_le_card ?_

Premises used: alternatingGroup.nontrivial_of_three_le_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
refine : 3 ≤ Nat.card α
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)

Tactic:
refine nontrivial_of_three_le_card ?_

Premises used: alternatingGroup.nontrivial_of_three_le_card