awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ False
have apply : sᶜ = univ
Tactic: apply compl_ne_univ.mpr h0.nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ sᶜ = univ
have apply : Nat.card α < sᶜ.ncard * 2
Tactic: apply hsc.eq_univ_of_card_lt
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ sᶜ ⊆ B
have not_isBlock_sc : ¬IsBlock (↥G) sᶜ
Tactic: have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    apply compl_ne_univ.mpr h0.nonempty -- `sᶜ ≠ univ`
    apply hsc.eq_univ_of_card_lt
    grind
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
⊢ sᶜ ⊆ B
have hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
Tactic: have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le h0
      (hBsc.ssubset_of_ne (by aesop)) -- uses Step 1
      hG.le hB
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
⊢ sᶜ ⊆ B
have hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
Tactic: have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) :
      B.Subsingleton :=
    have : IsPreprimitive (stabilizer G s) s :=
      stabilizer_subgroup_isPreprimitive h1 hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
⊢ sᶜ ⊆ B
have hBs : ¬B ⊆ s
Tactic: apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
hBs : ¬B ⊆ s
⊢ sᶜ ⊆ B
have hBsc : ¬B ⊆ sᶜ
Tactic: apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
⊢ sᶜ ⊆ B
have right : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
Tactic: suffices IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1) by
    apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le <;> grind
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
have this₁ : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
Tactic: have := isMultiplyPretransitive α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this_1 : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
hB_not_le_s : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBs : B ⊆ s), B.Subsingleton
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
have apply : s.ncard + 1 ≤ Nat.card α - 2
Tactic: apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (Nat.sub_le _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ Nontrivial α
have rw : 1 < Nat.card α
Tactic: rw [← Finite.one_lt_card_iff_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have this : Nontrivial α
Tactic: have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial]
    grind
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
this : Nontrivial α
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have obtain : ∀ (a : α) (ha : a ∈ s), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have rw : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) a)
Tactic: rw [Subsingleton.eq_singleton_of_mem h1 ha, stabilizer_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) a)
have this₁ : IsPreprimitive (↥(alternatingGroup α)) α
Tactic: have : IsPreprimitive (alternatingGroup α) α :=
    alternatingGroup.isPreprimitive_of_three_le_card α h3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : Nat.card α ≠ 2 * s.ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have hs₁ : ¬sᶜ.ncard = s.ncard
Tactic: rw [← ncard_add_ncard_compl s, two_mul, ne_eq, Nat.add_left_cancel_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have inr : ∀
  (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), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
Tactic: wlog hs' : ncard s < ncard sᶜ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
inr :
  ∀
    (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), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have wlog : ∀ {α : 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)
Tactic: wlog hs' : ncard s < ncard sᶜ
Cleared hypotheses: s, h0, h1, hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have inr : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)
Tactic: rw [← stabilizer_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)
have inr : sᶜᶜ.Nonempty
Tactic: apply this h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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ᶜᶜ.Nonempty
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)
have inr₁ : ¬sᶜᶜ.ncard = sᶜ.ncard
Tactic: apply this h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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ᶜᶜ.Nonempty
inr₁ : ¬sᶜᶜ.ncard = sᶜ.ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)
have inr₂ : sᶜ.ncard < sᶜᶜ.ncard
Tactic: apply this h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
have inr : ¬s.ncard = sᶜ.ncard
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
have inr : sᶜ.ncard < s.ncard
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have pos : ∀ (h0' : s.Nontrivial), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
Tactic: by_cases h0' : s.Nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have neg : ∀ (h0' : ¬s.Nontrivial), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
Tactic: by_cases h0' : s.Nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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)
have h0'₁ : s.Subsingleton
Tactic: simp only [not_nontrivial_iff] at h0'
Cleared hypotheses: h0'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
have apply : 3 ≤ Nat.card α
Tactic: apply isCoatom_stabilizer_singleton _ h0 h0'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
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
⊢ 3 ≤ Nat.card α
have rw : 3 ≤ s.ncard + sᶜ.ncard
Tactic: rw [← ncard_add_ncard_compl s]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ 3 ≤ s.ncard + sᶜ.ncard
have h0₁ : 0 < s.ncard
Tactic: rw [← ncard_pos] at h0 h1
Cleared hypotheses: h0, h1, hs, hs', h0'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
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
⊢ 3 ≤ s.ncard + sᶜ.ncard
have h1₁ : 0 < sᶜ.ncard
Tactic: rw [← ncard_pos] at h0 h1
Cleared hypotheses: h0, h1, hs, hs', h0'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
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}
    ↥(MonoidHom.range (G := Perm { x : α // x ∈ (↑s : Set α) }) (ofSubtype (p := fun (x : α) ↦ x ∈ (↑s : Set α))))
have this : IsMulCommutative.{u_1} (Perm ↥(↑s : Finset α))
Tactic: have : IsMulCommutative (Perm s) := isMulCommutative_iff_card_le_two.mpr (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
⊢ 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 α))))
    ⊤
have 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 α))
Tactic: rw [eq_top_iff, ← Equiv.Perm.closure_isSwap, Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
inst_2 : (s : Set α) → DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hab : 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 α))
have apply : Membership.mem (γ := Subgroup (Perm α))
  (MonoidHom.range (G :=
    Perm { x : α // x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} sorry) : Set α) })
    (ofSubtype (p := fun (x : α) ↦
      x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ Set.powersetCard α 2) {a, b} sorry) : Set α))))
  (swap a b)
Tactic: apply Subgroup.mem_iSup_of_mem ⟨{a, b}, Finset.card_pair hab⟩
-- 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
⊢ alternatingGroup α ≤ N
have rw : _root_.commutator (Perm α) ≤ N
Tactic: rw [← alternatingGroup.commutator_perm_eq hα]
-- 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
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)
have h_one_le : LE.le (α := ℕ) 1 2
Tactic: apply Set.powersetCard.isPreprimitive_perm
-- 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
h_one_le : LE.le (α := ℕ) 1 2
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)
have hn : 2 < Nat.card α
Tactic: apply Set.powersetCard.isPreprimitive_perm
-- 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
h_one_le : LE.le (α := ℕ) 1 2
hn : 2 < Nat.card α
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(Set.powersetCard α 2) : Type u_2)
have hα₁ : Nat.card α ≠ HMul.hMul (α := ℕ) 2 2
Tactic: apply Set.powersetCard.isPreprimitive_perm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Simple (hypothesis)
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
⊢ _root_.commutator (Perm α) ≤ N
have this : 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