-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₁ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₂ : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₃ have₄ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₅ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₆ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₇ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
    (g : Perm (↑s : Type u_1)), ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
inl :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
    (g : Perm (↑s : Type u_1))
    (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
    ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
inr inr₁ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
    (g : Perm (↑s : Type u_1))
    (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
    ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm

Tactic:
classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop

Premises used: Equiv.Perm.notMem_support, Set.disjoint_left, Submonoid.mk_smul, Equiv.Perm.mem_alternatingGroup, MulAction.mem_stabilizer_iff, Equiv.Perm.ofSubtype_mem_stabilizer, SemigroupAction.mul_smul