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.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ 1 < sᶜ.ncard

Tactic:
exact lt_of_le_of_lt h0.nonempty.ncard_pos hs

Premises used: lt_of_le_of_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ sᶜ.Nontrivial

Tactic:
have h1 : sᶜ.Nontrivial := by
    rw [← one_lt_ncard_iff_nontrivial]
    exact lt_of_le_of_lt h0.nonempty.ncard_pos hs
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
⊢ 1 < s.ncard

Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial] at h0

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
h0₁ : 1 < s.ncard
⊢ s.ncard < sᶜ.ncard

Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial] at h0

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
h0₁ : 1 < s.ncard
hs₁ : s.ncard < sᶜ.ncard
⊢ s.ncard + sᶜ.ncard = Nat.card α

Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial] at h0

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
h0₁ : 1 < s.ncard
hs₁ : s.ncard < sᶜ.ncard
this₁ : s.ncard + sᶜ.ncard = Nat.card α
⊢ sᶜ.Nontrivial

Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial] at h0

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : 1 < s.ncard
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
⊢ 4 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
⊢ 4 < Nat.card α

Tactic:
have hα : 4 < Nat.card α := by
    rw [← Set.one_lt_ncard_iff_nontrivial] at h0
    grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
right : ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
use stabilizer_ne_top h0.nonempty h1

Premises used: alternatingGroup.stabilizer_ne_top, Set.Nontrivial.nonempty
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
right : IsPreprimitive (↥G) α
⊢ G = ⊤

Tactic:
suffices IsPreprimitive G α from subgroup_eq_top_of_isPreprimitive hα G hG.le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
⊢ IsPretransitive (↥G) α

Tactic:
have := G.isPretransitive_of_stabilizer_lt hG
    (exists_mem_stabilizer_smul_eq (Nat.le_of_succ_le hα))
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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) α
right : ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B
⊢ IsPreprimitive (↥G) α

Tactic:
apply IsPreprimitive.mk

Premises used: MulAction.IsPreprimitive.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
right : ¬B.Subsingleton → B = univ
⊢ IsTrivialBlock B

Tactic:
rw [IsTrivialBlock, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
this : sᶜ ⊆ B
apply : Nat.card α < B.ncard * 2
⊢ B = univ

Tactic:
apply hB.eq_univ_of_card_lt

Premises used: MulAction.IsBlock.eq_univ_of_card_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
this : sᶜ ⊆ B
⊢ sᶜ.ncard ≤ B.ncard

Tactic:
have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
this_3 : sᶜ ⊆ B
this : sᶜ.ncard ≤ B.ncard
⊢ Nat.card α < B.ncard * 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
right : sᶜ ⊆ B
⊢ B = univ

Tactic:
suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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ᶜ
apply : sᶜ = univ
⊢ False

Tactic:
apply compl_ne_univ.mpr h0.nonempty

Premises used: Iff.mpr, Set.Nontrivial.nonempty, Set.compl_ne_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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ᶜ
apply : Nat.card α < sᶜ.ncard * 2
⊢ sᶜ = univ

Tactic:
apply hsc.eq_univ_of_card_lt

Premises used: MulAction.IsBlock.eq_univ_of_card_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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ᶜ
⊢ Nat.card α < sᶜ.ncard * 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
⊢ ¬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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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_1 : Set α
hB_1 : IsBlock (↥G) B_1
hB' : ¬B_1.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
B : Set α
hB : IsBlock (↥G) B
hBsc : B ⊆ sᶜ
⊢ B ≠ sᶜ

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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ᶜ
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
hBsc : ¬B ⊆ sᶜ
⊢ sᶜ ⊆ B

Tactic:
apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le

Premises used: MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl, LT.lt.le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
⊢ ¬B ⊆ s

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
⊢ ¬B ⊆ sᶜ

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
right : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
⊢ sᶜ ⊆ B

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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)) α (Nat.card α - 2)

Tactic:
have := isMultiplyPretransitive α
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
apply : s.ncard + 1 ≤ Nat.card α - 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)

Tactic:
apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (Nat.sub_le _ _)

Premises used: Nat.sub_le, MulAction.isMultiplyPretransitive_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
⊢ s.ncard + 1 ≤ Nat.card α - 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
rw : 1 < Nat.card α
⊢ Nontrivial α

Tactic:
rw [← Finite.one_lt_card_iff_nontrivial]

Premises used: Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ 1 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ Nontrivial α

Tactic:
have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial]
    grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
this : Nontrivial α
obtain : ∀ (a : α) (ha : a ∈ s), IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
obtain ⟨a, ha⟩ := h
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
rw : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) a)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
rw [Subsingleton.eq_singleton_of_mem h1 ha, stabilizer_singleton]

Premises used: Set.Subsingleton.eq_singleton_of_mem, MulAction.stabilizer_singleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsPreprimitive (↥(alternatingGroup α)) α

Tactic:
have : IsPreprimitive (alternatingGroup α) α :=
    alternatingGroup.isPreprimitive_of_three_le_card α h3
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this_1 : Nontrivial α
a : α
ha : a ∈ s
this : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) a)

Tactic:
apply IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive

Premises used: MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : Nat.card α ≠ 2 * s.ncard
⊢ ¬sᶜ.ncard = s.ncard

Tactic:
rw [← ncard_add_ncard_compl s, two_mul, ne_eq, Nat.add_left_cancel_iff] at hs

Premises used: two_mul, Nat.add_left_cancel_iff, Set.ncard_add_ncard_compl, ne_eq
-- 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
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)
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)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
wlog hs' : ncard s < ncard sᶜ

Premises used: Compl.compl, Set.ncard
-- 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 : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)

Tactic:
rw [← stabilizer_compl]

Premises used: stabilizer_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ᶜᶜ.Nonempty
inr₁ : ¬sᶜᶜ.ncard = sᶜ.ncard
inr₂ : sᶜ.ncard < sᶜᶜ.ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) sᶜ)

Tactic:
apply this h1
-- 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.Nonempty
⊢ sᶜᶜ.Nonempty

Tactic:
rw [compl_compl]

Premises used: compl_compl