awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
have inr : (↑g.support : Set α)ᶜ.ncard = n + 1
Tactic: apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
-- 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
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : (↑g.support : Set α)ᶜ.ncard = n + 1
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
have inr₁ : n + 2 < Nat.card α
Tactic: apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
-- 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
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : (↑g.support : Set α)ᶜ.ncard = n + 1
inr₁ : n + 2 < Nat.card α
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
have inr₂ : IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
-- 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
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ (↑g.support : Set α)ᶜ.ncard = n + 1
have inr : (↑g.support : Set α).ncard + (↑g.support : Set α)ᶜ.ncard = (↑g.support : Set α).ncard + (n + 1)
Tactic: apply Nat.add_left_cancel
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
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 α)ᶜ)
have this : IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: have := isPretransitive_of_isCycle_mem h3g.isCycle hg
-- 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
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 α)ᶜ)
have inr : Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))
Tactic: apply IsPreprimitive.of_prime_card
-- 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
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 α)ᶜ))
have h : Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 3
Tactic: convert! Nat.prime_three
-- 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
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
have h : Finset.card.{u_1} (α := α)
    {x : α |
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
  g.support.card
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
-- 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
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
have h : {x : α |
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
      (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
  g.support
Tactic: apply congr_arg
-- 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
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
have h : ∀ (x : α),
  Membership.mem (γ := Finset α)
      {x : α |
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x}
      x ↔
    x ∈ g.support
Tactic: ext x
-- 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
⊢ alternatingGroup α ≤ G
have inl : ∀ (hα4 : Nat.card α < 4), alternatingGroup α ≤ G
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]
-- 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
⊢ alternatingGroup α ≤ G
have inr : ∀ (hα4 : Nat.card α ≥ 4), alternatingGroup α ≤ G
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]
-- 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
⊢ alternatingGroup α ≤ G
have inr₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
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]
-- 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
⊢ alternatingGroup α ≤ G
have inr₃ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
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]
-- 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)
⊢ alternatingGroup α ≤ G
have inr₄ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
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]
-- 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)
⊢ alternatingGroup α ≤ G
have inr₅ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (n + 2)
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]
-- 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)
⊢ alternatingGroup α ≤ G
have inr₆ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), (↑g.support : Set α)ᶜ.ncard = n + 1
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]
-- 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
⊢ alternatingGroup α ≤ G
have inr₇ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
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]