awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
⊢ 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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
rw [← is_one_preprimitive_iff]

Premises used: MulAction.is_one_preprimitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
hn : LE.le (α := ℕ) 1 1
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1

Tactic:
rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]

Premises used: MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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 α (Nat.succ 1)

Tactic:
apply is_two_preprimitive hG hsn hsn' hprim

Premises used: MulAction.IsPreprimitive.is_two_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
⊢ LE.le (α := ℕ) 1 1

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)

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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
⊢ 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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)))
⊢ 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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
rw : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)

Tactic:
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]

Premises used: Nat.le_add_left, MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)

Tactic:
hrec ht_prim ?_ ?_ hGs' Subtype.finite

Premises used: Subtype.finite
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
refine_2 : n + 2 < Nat.card.{u_2} ↥(ofStabilizer G a)
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)

Tactic:
refine hrec ht_prim ?_ ?_ hGs' Subtype.finite

Premises used: Subtype.finite
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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 :
  (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard =
    n + 1
⊢ t.ncard = n + 1

Tactic:
rw [← Set.ncard_image_of_injective t Subtype.val_injective]

Premises used: Subtype.val_injective, Set.ncard_image_of_injective
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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 :
  (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
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:
apply Nat.add_right_cancel

Premises used: Nat.add_right_cancel
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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_2 : n + 2 + 1 < Nat.card α
⊢ n + 2 < Nat.card.{u_2} ↥(ofStabilizer G a)

Tactic:
rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]

Premises used: SubMulAction.nat_card_ofStabilizer_add_one_eq, Nat.add_lt_add_iff_right
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
⊢ n + 2 + 1 < Nat.card α

Tactic:
hsn'