-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
inl : ∀ (hα4 : Nat.card α < 4), alternatingGroup α ≤ G
inr inr₁ : ∀ (hα4 : Nat.card α ≥ 4), alternatingGroup α ≤ G
inr₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
inr₃ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
inr₄ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
inr₅ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (n + 2)
inr₆ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), (↑g.support : Set α)ᶜ.ncard = n + 1
inr₇ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
inr₈ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr₉ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
inr₁₀ inr₁₁ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr₁₂ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
    (this :
      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₁₃ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
    (this :
      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 :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
    (this :
      IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
        ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 3
h₁ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
    (this :
      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
⊢ alternatingGroup α ≤ G
have h₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
  (this :
    IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
  {x : α |
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support
Tactic: classical
  rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
  · -- trivial case : Fintype.card α ≤ 3
    rw [Nat.lt_succ_iff] at hα4
    apply alternatingGroup_le_of_index_le_two
    rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]
    apply le_trans (Nat.factorial_le hα4)
    rw [show Nat.factorial 3 = 2 * 3 by simp [Nat.factorial]]
    simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
    apply Nat.le_of_dvd Nat.card_pos
    suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_card
    simp only [orderOf_mk, h3g.orderOf]
    -- important case : Nat.card α ≥ 4
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
  apply IsMultiplyPretransitive.alternatingGroup_le
  suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
  rw [show Nat.card α - 2 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
  · apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      h3g.card_support, add_comm, hn]
  · grind
  have := isPretransitive_of_isCycle_mem h3g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_three
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
  apply congr_arg
  ext x
  simp [SubMulAction.mem_ofFixingSubgroup_iff]