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 : 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 = ⊤
⊢ G = ⊤
have inr : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3), G = ⊤
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]
-- 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 = ⊤
⊢ G = ⊤
have inr₂ : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3), G = ⊤
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]
-- 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 = ⊤
⊢ G = ⊤
have inr₃ : ∀ (this : Fintype α) (hα3 : Nat.card α ≥ 3) (n : ℕ) (hn : Nat.card α = n + 3)
  (hsc : (↑g.support : Set α)ᶜ.ncard = n + 1), G = ⊤
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]
-- 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 = ⊤
⊢ G = ⊤
have 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)
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]
-- 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)
⊢ G = ⊤
have 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)
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]
-- 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)
⊢ G = ⊤
have 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)
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]
-- 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)
⊢ G = ⊤
have 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 α
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]
-- 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 α
⊢ G = ⊤
have 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 α)ᶜ)
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]
-- 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: rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
-- 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: rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
-- 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
⊢ alternatingGroup α ≤ G
have hα4₁ : Nat.card α ≤ 3
Tactic: rw [Nat.lt_succ_iff] at hα4
Cleared hypotheses: hα4
-- 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 α ≤ 3
⊢ alternatingGroup α ≤ G
have inl : G.index ≤ 2
Tactic: apply alternatingGroup_le_of_index_le_two
-- 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 α ≤ 3
⊢ G.index ≤ 2
have inl : (Nat.card α).factorial ≤ 2 * Nat.card.{u_1} ↥G
Tactic: rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]
-- 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 α ≤ 3
⊢ (Nat.card α).factorial ≤ 2 * Nat.card.{u_1} ↥G
have inl : Nat.factorial 3 ≤ 2 * Nat.card.{u_1} ↥G
Tactic: apply le_trans (Nat.factorial_le hα4)
-- 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 α ≤ 3
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * Nat.card.{u_1} ↥G
have inl : 3 ≤ Nat.card.{u_1} ↥G
Tactic: simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
-- 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 α ≤ 3
⊢ 3 ≤ Nat.card.{u_1} ↥G
have inl : 3 ∣ Nat.card.{u_1} ↥G
Tactic: apply Nat.le_of_dvd Nat.card_pos
-- 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 α ≤ 3
this : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
⊢ 3 ∣ Nat.card.{u_1} ↥G
have rw : orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) ∣ Fintype.card.{u_1} ↥G
Tactic: rw [this, Nat.card_eq_fintype_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 α ≤ 3
⊢ 3 ∣ Nat.card.{u_1} ↥G
have inl : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
Tactic: suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_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
⊢ alternatingGroup α ≤ G
have inr : ∀ (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
Tactic: obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
-- 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
⊢ alternatingGroup α ≤ G
have inr : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
Tactic: apply IsMultiplyPretransitive.alternatingGroup_le
-- 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
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
have inr : IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
Tactic: suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
-- 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) α (Nat.card α - 2)
have inr : IsMultiplyPreprimitive (↥G) α (n + 2)
Tactic: rw [show Nat.card α - 2 = n + 2 by grind]