-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
have have₁ have₂ : ∀ (this : Fintype α), G = ⊤
inl : ∀ (this : Fintype α) (hα3 : Nat.card α < 3), G = ⊤
inr inr₁ : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3), G = ⊤
inr₂ : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3), G = ⊤
inr₃ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), G = ⊤
inr₄ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
inr₅ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
inr₆ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), IsMultiplyPreprimitive (↥G) α (n + 2)
inr₇ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), n + 2 < Nat.card α
inr₈ inr₉ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr₁₀ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1)
    (this_1 :
      IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
        ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr₁₁ :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1)
    (this_1 :
      IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
        ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))
h :
  ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
    (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1)
    (this_1 :
      IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
        ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 2
⊢ G = ⊤
have h₁ : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
  (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1)
  (this_1 :
    IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
  Finset.card.{u_1} (α := α)
      {x : α |
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support.card
Tactic: classical
  have := Fintype.ofFinite α
  rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
  · -- trivial case : Nat.card α ≤ 2
    rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card
  -- important case : Nat.card α ≥ 3
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
  have hsc : Set.ncard ((g.support)ᶜ : Set α) = n + 1 := by
    apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      card_support_eq_two.mpr h2g, add_comm, hn]
  apply eq_top_of_isMultiplyPretransitive
  suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
  rw [show Nat.card α - 1 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive hsc
  · rw [hn]; apply Nat.lt_add_one
  have := isPretransitive_of_isCycle_mem h2g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_two
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
  simp [SubMulAction.mem_ofFixingSubgroup_iff, support]