awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst_2 : N.Normal
ntN : Nontrivial.{u_2} ↥N
this : IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)
⊢ _root_.commutator (Perm α) ≤ N
have hNX : Ne.{u_2 + 1} (α := Set (↑(Set.powersetCard α 2) : Type u_2)) (fixedPoints ↥N (↑(Set.powersetCard α 2) : Type u_2))
  _root_.Set.univ
Tactic: apply iwasawaStructure_two.commutator_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst_2 : N.Normal
ntN : Nontrivial.{u_2} ↥N
this : IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)
⊢ _root_.commutator (Perm α) ≤ N
have hNX : Ne.{u_2 + 1} (α := Set (↑(Set.powersetCard α 2) : Type u_2)) (fixedPoints ↥N (↑(Set.powersetCard α 2) : Type u_2))
  _root_.Set.univ
Tactic: classical
  apply iwasawaStructure_two.commutator_le
  exact fixedPoints_ne_univ_of_faithfulSMul (by norm_num) (by grind)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : (↑(Set.powersetCard α 3) : Type u_1)
⊢ IsMulCommutative.{u_1} ↥(MonoidHom.range (ofSubtype (↑s : Finset α)))
have this : IsMulCommutative.{u_1} ↥(alternatingGroup ↥(↑s : Finset α))
Tactic: have : IsMulCommutative (alternatingGroup s) := isMulCommutative_of_card_le_three (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) ⊤
have rw : {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} ⊆
  (↑(⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) :
    Set ↥(alternatingGroup α))
Tactic: rw [eq_top_iff, ← closure_isThreeCycles_eq_top, Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : ↥(alternatingGroup α)
hg : Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} g
⊢ g ∈
    (↑(⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) :
      Set ↥(alternatingGroup α))
have apply : Membership.mem (γ := Subgroup ↥(alternatingGroup α))
  (MonoidHom.range
    (ofSubtype (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 3) (↑g : Perm α).support sorry) : Finset α)))
  g
Tactic: apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, hg.card_support⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : ↥(alternatingGroup α)
hg : Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (MonoidHom.range
      (ofSubtype
        (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 3) (↑g : Perm α).support ⋯) : Finset α)))
    g
have rw : (↑g : Perm α).support ⊆ (↑g : Perm α).support
Tactic: rw [mem_range_ofSubtype_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
⊢ N = ⊥ ∨ N = ⊤
have rw : Nontrivial.{u_1} ↥N → N = ⊤
Tactic: rw [or_iff_not_imp_left, ← ne_eq, ← Subgroup.nontrivial_iff_ne_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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
⊢ IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
have refine_1 : 3 < Nat.card α
Tactic: refine Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
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
⊢ N = ⊤
have this : IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)
Tactic: have : IsPreprimitive (alternatingGroup α) (Set.powersetCard α 3) := by
    refine Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num) ?_ ?_
    · exact lt_of_lt_of_le (by norm_num) hα
    · simpa using hα'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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)
⊢ N = ⊤
have rw : _root_.commutator ↥(alternatingGroup α) ≤ N
Tactic: rw [eq_top_iff, ← commutator_alternatingGroup_eq_top (by simpa using hα)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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)
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N
have hNX : Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 3) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 3) : Type u_1))
  Set.univ
Tactic: apply iwasawaStructure_three.commutator_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
k : ↥(alternatingGroup α)
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
have hs₁ : Nat.card.{u_1} ↥s = 4
Tactic: have hs : Nat.card s = 4 := by simpa
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
have 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})
Tactic: by_cases hk : (k : Perm α).support ⊆ s
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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})
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
have 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})
Tactic: by_cases hk : (k : Perm α).support ⊆ s
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
have 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})
Tactic: obtain ⟨σ, rfl⟩ := (mem_range_ofSubtype_iff s k).mpr hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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 (α := ↥(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})
have 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}
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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k ↔
    (↑k : Perm α).support ⊆ s ∧ ((↑k : Perm α) = 1 ∨ (↑k : Perm α).cycleType = {2, 2})
have neg : k ∉ Subgroup.map (ofSubtype s) (kleinFour ↥s)
Tactic: simp_rw [hk, false_and, iff_false]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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
⊢ k ∉ Subgroup.map (ofSubtype s) (kleinFour ↥s)
have neg : ∀ (hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s)) k),
  (↑k : Perm α).support ⊆ s
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
g : ↥(alternatingGroup α)
⊢ 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))
have 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))
Tactic: rcases g with ⟨g, hg⟩
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
hs : s.card = 4
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))
have 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))
Tactic: ext ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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 α
⊢ 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))
have h : 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) ↔
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.map (ofSubtype s) (kleinFour ↥s))
    (HSMul.hSMul (α := MulAut ↥(alternatingGroup α))
      (((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α))
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg))⁻¹ :
        MulAut ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) k hk))
Tactic: simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_map_kleinFour_ofSubtype hs,
    Subgroup.mk_smul, MulAut.smul_def, MulAut.inv_apply, MulAut.conj_symm_apply, Subgroup.coe_mul,
    Subgroup.coe_inv, ← ConjAct.toConjAct_inv_smul, Equiv.Perm.support_toConjAct_eq_smul_support,
    mem_map_kleinFour_ofSubtype (s := g • s) (by simpa), Finset.subset_smul_finset_iff,
    ConjAct.toConjAct_smul, cycleType_conj, mul_inv_eq_one, mul_eq_left]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
s : (↑(Set.powersetCard α 4) : Type u_1)
⊢ IsMulCommutative.{u_1} ↥(Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α)))
have this : IsMulCommutative.{u_1} ↥(kleinFour ↥(↑s : Finset α))
Tactic: have : IsMulCommutative (kleinFour s) :=
      (kleinFour_isKleinFour (by simp)).isMulCommutative
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (⨆ (s : (↑(Set.powersetCard α 4) : Type u_1)),
      Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α)))
    ⊤
have 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 α))
Tactic: rw [eq_top_iff, ← closure_cycleType_eq_two_two_eq_top h5, Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ g ∈
    (↑(⨆ (s : (↑(Set.powersetCard α 4) : Type u_1)),
          Subgroup.map (ofSubtype (↑s : Finset α)) (kleinFour ↥(↑s : Finset α))) :
      Set ↥(alternatingGroup α))
have apply : Membership.mem (γ := Subgroup ↥(alternatingGroup α))
  (Subgroup.map
    (ofSubtype (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support sorry) : Finset α))
    (kleinFour
      ↥(↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support sorry) : Finset α)))
  g
Tactic: apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, by simp [← sum_cycleType, hg]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).cycleType = {2, 2}
⊢ 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
have rw : (↑g : Perm α).support ⊆
    (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support sorry) : Finset α) ∧
  ((↑g : Perm α) = 1 ∨ (↑g : Perm α).cycleType = {2, 2})
Tactic: rw [mem_map_kleinFour_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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})
⊢ 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
have hs : (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 4) (↑g : Perm α).support sorry) : Finset α).card = 4
Tactic: rw [mem_map_kleinFour_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
⊢ N = ⊥ ∨ N = ⊤
have rw : Nontrivial.{u_1} ↥N → N = ⊤
Tactic: rw [or_iff_not_imp_left, ← ne_eq, ← Subgroup.nontrivial_iff_ne_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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)
have hn : 4 < Nat.card α
Tactic: apply Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
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
⊢ N = ⊤
have this : 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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)
⊢ N = ⊤
have rw : _root_.commutator ↥(alternatingGroup α) ≤ N
Tactic: rw [eq_top_iff, ← commutator_alternatingGroup_eq_top hα]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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)
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N
have hNX : Ne.{u_1 + 1} (α := Set (↑(Set.powersetCard α 4) : Type u_1)) (fixedPoints ↥N (↑(Set.powersetCard α 4) : Type u_1))
  Set.univ
Tactic: apply (iwasawaStructure_four hα).commutator_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
⊢ N = ⊥ ∨ N = ⊤
have pos : ∀ (hα' : Nat.card α = 6), N = ⊥ ∨ N = ⊤
Tactic: by_cases hα' : Nat.card α = 6
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
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 = ⊤
⊢ N = ⊥ ∨ N = ⊤
have neg : ∀ (hα' : ¬Nat.card α = 6), N = ⊥ ∨ N = ⊤
Tactic: by_cases hα' : Nat.card α = 6
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
⊢ ∃ (x : ↥(alternatingGroup α)) (y : ↥(alternatingGroup α)), x ≠ y
have rw : Nontrivial.{u_1} ↥(alternatingGroup α)
Tactic: rw [← _root_.nontrivial_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα : 5 ≤ Nat.card α
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)
have refine : 3 ≤ Nat.card α
Tactic: refine nontrivial_of_three_le_card ?_