awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_2 : DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty)
    (hs : ¬sᶜ.ncard = s.ncard) (hs' : s.ncard < sᶜ.ncard),
    IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
inr : ¬s.ncard = sᶜ.ncard
⊢ ¬sᶜᶜ.ncard = sᶜ.ncard

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_2 : DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty)
    (hs : ¬sᶜ.ncard = s.ncard) (hs' : s.ncard < sᶜ.ncard),
    IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
inr : sᶜ.ncard < s.ncard
⊢ sᶜ.ncard < sᶜᶜ.ncard

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_2 : DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty)
    (hs : ¬sᶜ.ncard = s.ncard) (hs' : s.ncard < sᶜ.ncard),
    IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ s.Nonempty

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_2 : DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty)
    (hs : ¬sᶜ.ncard = s.ncard) (hs' : s.ncard < sᶜ.ncard),
    IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ ¬s.ncard = sᶜ.ncard

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_2 : DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty)
    (hs : ¬sᶜ.ncard = s.ncard) (hs' : s.ncard < sᶜ.ncard),
    IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ sᶜ.ncard < s.ncard

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
pos : ∀ (h0' : s.Nontrivial), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
neg : ∀ (h0' : ¬s.Nontrivial), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
by_cases h0' : s.Nontrivial

Premises used: Set.Nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Nontrivial
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
apply isCoatom_stabilizer_of_ncard_lt_ncard_compl h0' hs'

Premises used: alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : ¬s.Nontrivial
⊢ s.Subsingleton

Tactic:
simp only [not_nontrivial_iff] at h0'

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
apply : 3 ≤ Nat.card α
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
apply isCoatom_stabilizer_singleton _ h0 h0'

Premises used: alternatingGroup.isCoatom_stabilizer_singleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
rw : 3 ≤ s.ncard + sᶜ.ncard
⊢ 3 ≤ Nat.card α

Tactic:
rw [← ncard_add_ncard_compl s]

Premises used: Set.ncard_add_ncard_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
⊢ 0 < s.ncard

Tactic:
rw [← ncard_pos] at h0 h1

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
h0₁ : 0 < s.ncard
⊢ 0 < sᶜ.ncard

Tactic:
rw [← ncard_pos] at h0 h1

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
h0₁ : 0 < s.ncard
h1₁ : 0 < sᶜ.ncard
⊢ ¬sᶜ.ncard = s.ncard

Tactic:
rw [← ncard_pos] at h0 h1

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
h0₁ : 0 < s.ncard
h1₁ : 0 < sᶜ.ncard
hs₁ : ¬sᶜ.ncard = s.ncard
⊢ s.ncard < sᶜ.ncard

Tactic:
rw [← ncard_pos] at h0 h1

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
h0₁ : 0 < s.ncard
h1₁ : 0 < sᶜ.ncard
hs₁ : ¬sᶜ.ncard = s.ncard
hs'₁ : s.ncard < sᶜ.ncard
⊢ s.Subsingleton

Tactic:
rw [← ncard_pos] at h0 h1

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α_1 : Type u_1
inst : Fintype α_1
inst_1 : DecidableEq α_1
α : Type u_1
inst_2 : Fintype α
inst_3 : DecidableEq α
s : Set α
h0 : 0 < s.ncard
h1 : 0 < sᶜ.ncard
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
⊢ 3 ≤ s.ncard + sᶜ.ncard

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
s : (↑(Set.powersetCard α 2) : Type u_1)
⊢ Nat.card.{u_1} ↥(↑s : Finset α) ≤ 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
s : (↑(Set.powersetCard α 2) : Type u_1)
⊢ IsMulCommutative.{u_1} (Perm ↥(↑s : Finset α))

Tactic:
have : IsMulCommutative (Perm s) := isMulCommutative_iff_card_le_two.mpr (by simp)
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
s : (↑(Set.powersetCard α 2) : Type u_1)
this : IsMulCommutative.{u_1} (Perm ↥(↑s : Finset α))
⊢ IsMulCommutative.{u_1}
    ↥(MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α))))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
g : Perm α
s : (↑(Set.powersetCard α 2) : Type u_1)
⊢ MonoidHom.range (G := Perm ↥(g • (↑s : Finset α))) (ofSubtype (p := fun (x : α) ↦ x ∈ g • (↑s : Finset α))) =
    HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
      (MonoidHom.range (G := Perm ↥(↑s : Finset α)) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Finset α))))

Tactic:
(conj_smul_range_ofSubtype g s).symm

Premises used: Eq.symm, Subtype.val, Equiv.Perm.conj_smul_range_ofSubtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
g : Perm α
s : (↑(Set.powersetCard α 2) : Type u_1)
⊢ MonoidHom.range (G := Perm { x : α // x ∈ (↑(g • s) : Set α) })
      (ofSubtype (p := fun (x : α) ↦ x ∈ (↑(g • s) : Set α))) =
    HSMul.hSMul (α := MulAut (Perm α)) (β := Subgroup (Perm α))
      ((MulAut.conj : (a : Perm α) → MulAut (Perm α)) g : MulAut (Perm α))
      (MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α))))

Tactic:
convert! (conj_smul_range_ofSubtype g s).symm

Premises used: Eq.symm, Subtype.val, Equiv.Perm.conj_smul_range_ofSubtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
rw :
  {σ : Perm α | σ.IsSwap} ⊆
    (↑(⨆ (s : (↑(Set.powersetCard α 2) : Type u_1)),
          MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α)))) :
      Set (Perm α))
⊢ Eq.{u_1 + 1} (α := Subgroup (Perm α))
    (⨆ (s : (↑(Set.powersetCard α 2) : Type u_1)),
      MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α))))
    ⊤

Tactic:
rw [eq_top_iff, ← Equiv.Perm.closure_isSwap, Subgroup.closure_le]

Premises used: Equiv.Perm.closure_isSwap, eq_top_iff, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hab : a ≠ b
apply :
  Membership.mem (γ := Subgroup (Perm α))
    (MonoidHom.range (G :=
      Perm { x : α // x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α) })
      (ofSubtype (p := fun (x : α) ↦
        x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α))))
    (swap a b)
⊢ swap a b ∈
    (↑(⨆ (s : (↑(Set.powersetCard α 2) : Type u_1)),
          MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α)))) :
      Set (Perm α))

Tactic:
apply Subgroup.mem_iSup_of_mem ⟨{a, b}, Finset.card_pair hab⟩

Premises used: Subgroup.mem_iSup_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ a ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ b ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ Membership.mem (γ := Subgroup (Perm α))
    (MonoidHom.range (G :=
      Perm { x : α // x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α) })
      (ofSubtype (p := fun (x : α) ↦
        x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} ⋯) : Set α))))
    (swap a b)

Tactic:
exact ⟨swap ⟨a, by simp⟩ ⟨b, by simp⟩, Equiv.Perm.ofSubtype_swap_eq _ _⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
rw : _root_.commutator (Perm α) ≤ N
⊢ alternatingGroup α ≤ N

Tactic:
rw [← alternatingGroup.commutator_perm_eq hα]

Premises used: alternatingGroup.commutator_perm_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
h_one_le : LE.le (α := ℕ) 1 2
hn : 2 < Nat.card α
hα₁ : Nat.card α ≠ HMul.hMul (α := ℕ) 2 2
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)

Tactic:
apply Set.powersetCard.isPreprimitive_perm

Premises used: Set.powersetCard.isPreprimitive_perm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
⊢ LE.le (α := ℕ) 1 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
⊢ 2 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
⊢ Nat.card α ≠ HMul.hMul (α := ℕ) 2 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)

Tactic:
have : IsPreprimitive (Perm α) (Set.powersetCard α 2) := by
    apply Set.powersetCard.isPreprimitive_perm <;> grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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)
hNX :
  Ne.{u_2 + 1} (α := Set (↑(Set.powersetCard α 2) : Type u_2)) (fixedPoints ↥N (↑(Set.powersetCard α 2) : Type u_2))
    _root_.Set.univ
⊢ _root_.commutator (Perm α) ≤ N

Tactic:
apply iwasawaStructure_two.commutator_le

Premises used: MulAction.IwasawaStructure.commutator_le, Equiv.Perm.iwasawaStructure_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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)
⊢ LT.lt (α := ℕ) 0 2

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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)
⊢ 2 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
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)
⊢ Ne.{u_2 + 1} (α := Set (↑(Set.powersetCard α 2) : Type u_2)) (fixedPoints ↥N (↑(Set.powersetCard α 2) : Type u_2))
    _root_.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_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)
hNX :
  Ne.{u_2 + 1} (α := Set (↑(Set.powersetCard α 2) : Type u_2)) (fixedPoints ↥N (↑(Set.powersetCard α 2) : Type u_2))
    _root_.Set.univ
⊢ _root_.commutator (Perm α) ≤ N

Tactic:
classical
  apply iwasawaStructure_two.commutator_le
  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 : (↑(Set.powersetCard α 3) : Type u_1)
⊢ Nat.card.{u_1} ↥(↑s : Finset α) ≤ 3

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : (↑(Set.powersetCard α 3) : Type u_1)
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup ↥(↑s : Finset α))

Tactic:
have : IsMulCommutative (alternatingGroup s) := isMulCommutative_of_card_le_three (by simp)
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : (↑(Set.powersetCard α 3) : Type u_1)
this : IsMulCommutative.{u_1} ↥(alternatingGroup ↥(↑s : Finset α))
⊢ IsMulCommutative.{u_1} ↥(MonoidHom.range (ofSubtype (↑s : Finset α)))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
rw :
  {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} ⊆
    (↑(⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) :
      Set ↥(alternatingGroup α))
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) ⊤

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

Premises used: eq_top_iff, alternatingGroup.closure_isThreeCycles_eq_top, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : ↥(alternatingGroup α)
hg : Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} g
apply :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (MonoidHom.range
      (ofSubtype
        (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 3) (↑g : Perm α).support ⋯) : Finset α)))
    g
⊢ g ∈
    (↑(⨆ (s : (↑(Set.powersetCard α 3) : Type u_1)), MonoidHom.range (ofSubtype (↑s : Finset α))) :
      Set ↥(alternatingGroup α))

Tactic:
apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, hg.card_support⟩

Premises used: Subgroup.mem_iSup_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : ↥(alternatingGroup α)
hg : Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle} g
rw rw₁ : (↑g : Perm α).support ⊆ (↑g : Perm α).support
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α))
    (MonoidHom.range
      (ofSubtype
        (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 3) (↑g : Perm α).support ⋯) : Finset α)))
    g

Tactic:
rw [mem_range_ofSubtype_iff]

Premises used: alternatingGroup.mem_range_ofSubtype_iff
-- 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
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 α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ LE.le (α := ℕ) 3 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
refine_1 : 3 < Nat.card α
refine_2 : Nat.card α ≠ HMul.hMul (α := ℕ) 2 3
⊢ IsPreprimitive.{u_1, u_1} ↥(alternatingGroup α) (↑(Set.powersetCard α 3) : Type u_1)

Tactic:
refine 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 α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst_2 : N.Normal
hN : Nontrivial.{u_1} ↥N
⊢ LT.lt (α := ℕ) 3 5

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
⊢ 3 < Nat.card α

Tactic:
exact lt_of_lt_of_le (by norm_num) hα

Premises used: lt_of_lt_of_le
-- 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
⊢ Nat.card α ≠ HMul.hMul (α := ℕ) 2 3

Tactic:
simpa using hα'
-- 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
⊢ 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α'
-- 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)
⊢ 5 ≤ Nat.card α

Tactic:
simpa using hα
-- 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)
rw : _root_.commutator ↥(alternatingGroup α) ≤ N
⊢ N = ⊤

Tactic:
rw [eq_top_iff, ← commutator_alternatingGroup_eq_top (by simpa using hα)]

Premises used: eq_top_iff, commutator_alternatingGroup_eq_top