awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h⁻¹ • a = (↑b : α)
⊢ h • Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • h⁻¹ • a = a
have a₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) (h * g * h⁻¹)
Tactic: simp only [subgroup_smul_def, smul_smul, ← mul_assoc, ← mem_stabilizer_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero <| ne_zero_of_lt hsn'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
⊢ False
have hsn₁ : Nat.card α = n + 1
Tactic: rw [hs, Set.ncard_univ] at hsn
Cleared hypotheses: hsn, hsn', this, hs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have hs_ne_univ : s ≠ Set.univ
Tactic: have hs_ne_univ : s ≠ Set.univ := by
    intro hs
    rw [hs, Set.ncard_univ] at hsn
    simp only [hsn, add_lt_add_iff_left, Nat.not_ofNat_lt_one] at hsn'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have hs_nonempty : s.Nonempty
Tactic: have hs_nonempty : s.Nonempty := by
    simp [← Set.ncard_pos s.toFinite, hsn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : ∀ (hn : n + 1 < 2),
  (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Tactic: rcases Nat.lt_or_ge (n + 1) 2 with hn | hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
h :
  ∀ (hn : n + 1 < 2),
    (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
      (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h₁ : ∀ (hn : n + 1 ≥ 2),
  (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Tactic: rcases Nat.lt_or_ge (n + 1) 2 with hn | hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 < 2
⊢ n = 0
have rwa : ∀ (hn : n < 1), n = 0
Tactic: rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 < 2
rwa : ∀ (hn : n < 1), n = 0
⊢ n = 0
have rwa₁ : ∀ (hn : n = 0), n = 0
Tactic: rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 < 2
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have hn₁ : n = 0
Tactic: have hn : n = 0 := by
      rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have hsn₁ : ∃ (a : α), s = {a}
Tactic: simp only [hn, zero_add, Set.ncard_eq_one] at hsn
Cleared hypotheses: hsn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
hsn : ∃ (a : α), s = {a}
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : ∀ (a : α) (hsa : s = {a}),
  (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Tactic: obtain ⟨a, hsa⟩ := hsn
Cleared hypotheses: hsn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have refine : ∀ (hs_prim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)), IsMultiplyPreprimitive G α 2
Tactic: refine ⟨this, fun hs_prim ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α 2
have hs_prim₁ : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a})
Tactic: rw [hsa] at hs_prim
Cleared hypotheses: hs_prim
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a})
⊢ IsMultiplyPreprimitive G α 2
have rw : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
Tactic: rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Tactic: suffices IsPretransitive (fixingSubgroup G s) (ofFixingSubgroup G s) →
      IsMultiplyPretransitive G α 2 by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      rw [hsa] at hs_prim
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]
      exact IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) → IsMultiplyPretransitive G α 2
Tactic: rw [hsa]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) → IsMultiplyPretransitive G α 2
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) →
  IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
Tactic: rw [ofStabilizer.isMultiplyPretransitive (a := a)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn_1 : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) →
    IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) →
  IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
Tactic: rw [is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : ∀ (hn1 : 2 * (n + 1) < Nat.card α),
  (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Tactic: rcases Nat.lt_or_ge (2 * (n + 1)) (Nat.card α) with hn1 | hn2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
h :
  ∀ (hn1 : 2 * (n + 1) < Nat.card α),
    (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
      (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h₁ : ∀ (hn2 : 2 * (n + 1) ≥ Nat.card α),
  (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Tactic: rcases Nat.lt_or_ge (2 * (n + 1)) (Nat.card α) with hn1 | hn2