awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ t.ncard = n + 1
have refine_1 : (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t).ncard =
  n + 1
Tactic: rw [← Set.ncard_image_of_injective t Subtype.val_injective]
-- 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)
⊢ (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard =
    n + 1
have refine_1 : (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard +
    1 =
  n + 1 + 1
Tactic: apply Nat.add_right_cancel
-- 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 α
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)
have succ : ∃ (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)
Tactic: suffices ∃ (a : α) (t : Set (SubMulAction.ofStabilizer G a)),
      a ∈ s ∧ s = insert a (Subtype.val '' t) by
      obtain ⟨a, t, _, hst⟩ := this
      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
      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
      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
      have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
      refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
      · -- t.card = Nat.succ n
        rw [← Set.ncard_image_of_injective t Subtype.val_injective]
        apply Nat.add_right_cancel
        rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
      · -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
        rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
        exact 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 : s.Nonempty
⊢ ∃ (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)
have obtain : ∀ (a : α) (ha : a ∈ s),
  ∃ (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)
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this
-- 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 : α
ha : a ∈ s
⊢ ∃ (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)
have right : s =
  insert a
    (Set.image (α := ↥(ofStabilizer G a))
      (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
        s))
Tactic: use a, Subtype.val ⁻¹' s, ha
-- 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 : α
ha : a ∈ s
⊢ s =
    insert a
      (Set.image (α := ↥(ofStabilizer G a))
        (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
          s))
have right : ∀ (x : α),
  x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))
Tactic: ext x
-- 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 : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))
have pos : ∀ (hx : x = a),
  x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))
Tactic: by_cases hx : x = 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 : α
ha : a ∈ s
x : α
pos :
  ∀ (hx : x = a),
    x ∈ s ↔
      x ∈
        insert a
          (Set.image (α := ↥(ofStabilizer G a))
            (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
              s))
⊢ x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))
have neg : ∀ (hx : ¬x = a),
  x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))
Tactic: by_cases hx : x = 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)),
    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)
have succ : s.Nonempty
Tactic: suffices s.Nonempty by
      obtain ⟨a, ha⟩ := this
      use a, Subtype.val ⁻¹' s, ha
      ext x
      by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]
-- 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 α
⊢ s.Nonempty
have succ : 0 < n + 1 + 1
Tactic: rw [← Set.ncard_pos, hsn]
-- 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 α
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)
hα : Finite α
⊢ IsMultiplyPreprimitive G α (n + 2)
have zero : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
  (hsn : s.ncard = HAdd.hAdd (α := ℕ) 0 1) (hsn' : HAdd.hAdd (α := ℕ) 0 2 < Nat.card α)
  (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
  IsMultiplyPreprimitive G α (HAdd.hAdd (α := ℕ) 0 2)
Tactic: induction n generalizing α hα G with
  -- case n = 0
  | zero => simpa using is_two_preprimitive hG hsn hsn' hprim
  -- Induction step
  | succ n hrec =>
    suffices ∃ (a : α) (t : Set (SubMulAction.ofStabilizer G a)),
      a ∈ s ∧ s = insert a (Subtype.val '' t) by
      obtain ⟨a, t, _, hst⟩ := this
      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
      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
      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
      have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
      refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
      · -- t.card = Nat.succ n
        rw [← Set.ncard_image_of_injective t Subtype.val_injective]
        apply Nat.add_right_cancel
        rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
      · -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
        rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
        exact hsn'
    -- ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
    suffices s.Nonempty by
      obtain ⟨a, ha⟩ := this
      use a, Subtype.val ⁻¹' s, ha
      ext x
      by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]
    rw [← Set.ncard_pos, hsn]; apply Nat.succ_pos
Cleared hypotheses: G, α, inst, inst_1, hG, s, n, hsn, hsn', hprim, hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
⊢ G = ⊤
have h : Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥G
Tactic: apply Subgroup.eq_top_of_le_card
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
⊢ Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥G
have h : (Nat.card α).factorial ≤ Nat.card.{u_1} ↥G
Tactic: rw [Nat.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
⊢ (Nat.card α).factorial ≤ Nat.card.{u_1} ↥G
have h : Nat.factorial 2 ≤ Nat.card.{u_1} ↥G
Tactic: apply (Nat.factorial_le hα).trans
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
⊢ Nat.factorial 2 ≤ Nat.card.{u_1} ↥G
have h : 2 ≤ Nat.card.{u_1} ↥G
Tactic: rwa [Nat.factorial_two, Nat.succ_le_iff, one_lt_card_iff_ne_bot, ← nontrivial_iff_ne_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : 2 ≤ Nat.card.{u_1} ↥G
⊢ Nat.factorial 2 ≤ Nat.card.{u_1} ↥G
have h₁ : 1 < Nat.card.{u_1} ↥G
Tactic: rwa [Nat.factorial_two, Nat.succ_le_iff, one_lt_card_iff_ne_bot, ← nontrivial_iff_ne_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : 2 ≤ Nat.card.{u_1} ↥G
h₁ : 1 < Nat.card.{u_1} ↥G
⊢ Nat.factorial 2 ≤ Nat.card.{u_1} ↥G
have h₂ : G ≠ ⊥
Tactic: rwa [Nat.factorial_two, Nat.succ_le_iff, one_lt_card_iff_ne_bot, ← nontrivial_iff_ne_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
⊢ IsMultiplyPretransitive K α n
have this : Finite α
Tactic: have : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by
    simp [Nat.card_eq_zero_of_infinite] at hα)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this : Finite α
⊢ IsMultiplyPretransitive K α n
have have : ∀ (this : Fintype α), IsMultiplyPretransitive K α n
Tactic: have : Fintype α := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
⊢ IsMultiplyPretransitive K α n
have pos : ∀ (hn : n ≤ 2), IsMultiplyPretransitive K α n
Tactic: by_cases hn : n ≤ 2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
pos : ∀ (hn : n ≤ 2), IsMultiplyPretransitive K α n
⊢ IsMultiplyPretransitive K α n
have neg : ∀ (hn : ¬n ≤ 2), IsMultiplyPretransitive K α n
Tactic: by_cases hn : n ≤ 2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : n ≤ 2
⊢ IsMultiplyPretransitive K α n
have pos : (↑2 : ℕ∞) ≤ ENat.card α
Tactic: apply MulAction.isMultiplyPretransitive_of_le' hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
⊢ IsMultiplyPretransitive K α n
have neg : IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
Tactic: suffices (IsEmpty (Fin n ↪ α)) by infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
⊢ IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
have neg : ¬Nonempty.{u_1 + 1} (Fin n ↪ α)
Tactic: rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
neg : ¬Nonempty.{u_1 + 1} (Fin n ↪ α)
⊢ IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
have neg₁ : ¬Fintype.card (Fin n) ≤ Fintype.card α
Tactic: rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]