awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)
Tactic: apply (hrec _ hmn hG htm htm').1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α (n + 2)
have hα : Finite α
Tactic: have hα : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by
    simp [Nat.card_eq_zero_of_infinite] at hsn')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
this :
  ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
    a ∈ s ∧
      s =
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have obtain : ∀ (a : α) (t : Set ↥(ofStabilizer G a)),
  a ∈ s →
    ∀
      (hst :
        s =
          insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
              t)),
      IsMultiplyPreprimitive G α (n + 1 + 2)
Tactic: obtain ⟨a, t, _, hst⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
h :
  a ∈
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ False
have h₁ : ∃ x ∈ t, (↑x : α) = a
Tactic: rw [Set.mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
h : ∃ x ∈ t, (↑x : α) = a
⊢ False
have obtain : ∀ (x : ↥(ofStabilizer G a)) (hx : x ∈ t ∧ (↑x : α) = a), False
Tactic: obtain ⟨x, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
x : ↥(ofStabilizer G a)
hx : x ∈ t ∧ (↑x : α) = a
⊢ False
have apply : Membership.mem (γ := Set α) {a} (↑x : α)
Tactic: apply x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
x : ↥(ofStabilizer G a)
hx : x ∈ t ∧ (↑x : α) = a
⊢ Membership.mem (γ := Set α) {a} (↑x : α)
have rw : Membership.mem (γ := Set α) {a} a
Tactic: rw [hx.right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have ha' : a ∉
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
    t
Tactic: have ha' : a ∉ Subtype.val '' t := by
        intro h; rw [Set.mem_image] at h; obtain ⟨x, hx⟩ := h
        apply x.prop; rw [hx.right]; exact Set.mem_singleton a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
have rw : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
Tactic: rw [← is_one_preprimitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
have rw : IsMultiplyPreprimitive G α (Nat.succ 1)
Tactic: rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
rw : IsMultiplyPreprimitive G α (Nat.succ 1)
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
have hn : LE.le (α := ℕ) 1 1
Tactic: rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
Tactic: have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
        rw [← is_one_preprimitive_iff]
        rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
        · apply is_two_preprimitive hG hsn hsn' hprim
        · norm_num
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have this : IsPreprimitive.{u_1, u_2}
  ↥(fixingSubgroup G
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
          t)))
  ↥(ofFixingSubgroup G
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
          t)))
Tactic: have : IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
          (ofFixingSubgroup G (insert a (Subtype.val '' t))) :=
        IsPreprimitive.of_surjective
          (ofFixingSubgroup_of_eq_bijective (hst := hst)).surjective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
    ↥(ofFixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have hGs' : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
Tactic: have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
    ↥(ofFixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
hGs' : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have rw : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
Tactic: rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
    ↥(ofFixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
hGs' : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
have refine_1 : t.ncard = n + 1
Tactic: refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 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 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
    ↥(ofFixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
hGs' : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
refine_1 : t.ncard = n + 1
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
have refine_2 : n + 2 < Nat.card.{u_2} ↥(ofStabilizer G a)
Tactic: refine hrec ht_prim ?_ ?_ hGs' Subtype.finite