-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
have have₁ have₂ : ∀ (h1 : sᶜ.Nonempty), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have₃ : ∀ (h1 : sᶜ.Nonempty) (this : Fintype α), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have₄ : ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G), G = ⊤
have₅ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G), G = ⊤
have₆ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G), G = ⊤
have₇ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G), IsPreprimitive (↥G) α
have₈ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α),
    IsPreprimitive (↥G) α
isTrivialBlock_of_isBlock isTrivialBlock_of_isBlock₁ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α)
    {B : Set α} (hB : IsBlock (↥G) B), IsTrivialBlock B
isTrivialBlock_of_isBlock₂ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α)
    {B : Set α} (hB : IsBlock (↥G) B), B.Subsingleton ∨ B = univ
isTrivialBlock_of_isBlock₃ isTrivialBlock_of_isBlock₄ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α)
    {B : Set α} (hB : IsBlock (↥G) B) (hB' : ¬B.Subsingleton), B = univ
isTrivialBlock_of_isBlock₅ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α)
    {B : Set α} (hB : IsBlock (↥G) B) (hB' : ¬B.Subsingleton), sᶜ ⊆ B
isTrivialBlock_of_isBlock₆ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G) (this : IsPretransitive (↥G) α)
    {B : Set α} (hB : IsBlock (↥G) B) (hB' : ¬B.Subsingleton) (not_isBlock_sc : ¬IsBlock (↥G) sᶜ), sᶜ ⊆ B
isTrivialBlock_of_isBlock₇ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ 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
isTrivialBlock_of_isBlock₈ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ 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
isTrivialBlock_of_isBlock₉ :
  ∀ (h1 : sᶜ.Nonempty) (this : Fintype α) (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G)
    (hG' : stabilizer (Perm α) sᶜ < G) (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ 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 (Perm α) α (s.ncard + 1) → sᶜ ⊆ B
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)

Tactic:
classical
  have h1 : sᶜ.Nonempty := nonempty_iff_ne_empty.mpr (by aesop)
  have : Fintype α := Fintype.ofFinite α
  -- To prove that `stabilizer (Perm α) s` is maximal,
  -- we need to prove that it is `≠ ⊤`
  refine ⟨stabilizer_ne_top_of_nonempty_of_nonempty_compl h0 h1, fun G hG ↦ ?_⟩
  have hG' : stabilizer (Perm α) sᶜ < G := by rwa [stabilizer_compl]
  -- … and that every strict over-subgroup `G` is equal to `⊤`
  -- We know that `G` contains a swap
  obtain ⟨g, hg_swap, hg⟩ := has_swap_mem_of_lt_stabilizer s G hG
  -- By Jordan's theorem `subgroup_eq_top_of_isPreprimitive_of_isSwap_mem`,
  -- it suffices to prove that `G` acts primitively
  apply subgroup_eq_top_of_isPreprimitive_of_isSwap_mem _ g hg_swap hg
  -- First, we prove that `G` acts transitively
  have := G.isPretransitive_of_stabilizer_lt hG exists_mem_stabilizer_smul_eq
  apply IsPreprimitive.mk
  -- We now have to prove that all blocks of `G` are trivial
  -- We reduce to proving that a block which is not a subsingleton is `univ`.
  intro B hB
  unfold IsTrivialBlock
  rw [or_iff_not_imp_left]
  intro hB'
  suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia
  -- The proof needs 4 steps
  /- Step 1 : `sᶜ` is not a block.
       This uses that `Nat.card s < Nat.card sᶜ`.
       In the equality case, `Nat.card s` = Nat.card sᶜ`,
       it would be possible that `sᶜ` is a block,
       and then `G` would be a wreath product,
       — this is case (b) of the O'Nan-Scott classification
       of maximal subgroups of the symmetric group -/
  have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
  -- Step 2 : A block contained in sᶜ is a subsingleton
  have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    -- uses Step 1
    hB.subsingleton_of_ssubset_of_stabilizer_Perm_le (hBsc.ssubset_of_ne (by lia)) hG'.le
  -- Step 3 : A block contained in `s` is a subsingleton
  have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) : B.Subsingleton :=
    have := isPreprimitive_stabilizer_subgroup hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
  -- Step 4 : `sᶜ ⊆ B`
  have _ := isMultiplyPretransitive α (s.ncard + 1)
  apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;>
    grind

Premises used: Classical.or_iff_not_imp_left, MulAction.IsPreprimitive.mk, MulAction.IsTrivialBlock