awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
⊢ s.Nonempty

Tactic:
simp [← Set.ncard_pos s.toFinite, hsn]

Premises used: Set.toFinite, Set.ncard_pos
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
⊢ s.Nonempty

Tactic:
have hs_nonempty : s.Nonempty := by
    simp [← Set.ncard_pos s.toFinite, hsn]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
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)

Tactic:
rcases Nat.lt_or_ge (n + 1) 2 with hn | hn

Premises used: HAdd.hAdd, Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hn : n = 0), n = 0
⊢ n = 0

Tactic:
rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn

Premises used: Nat.succ_lt_succ_iff, Nat.lt_one_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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

Tactic:
have hn : n = 0 := by
      rwa [Nat.succ_lt_succ_iff, Nat.lt_one_iff] at hn
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
⊢ ∃ (a : α), s = {a}

Tactic:
simp only [hn, zero_add, Set.ncard_eq_one] at hsn

Premises used: Set.ncard_eq_one, zero_add
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}
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)
⊢ (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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)

Tactic:
⟨this, fun hs_prim ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
refine :
  ∀ (hs_prim : 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)

Tactic:
refine ⟨this, fun hs_prim ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a})

Tactic:
rw [hsa] at hs_prim
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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})
rw : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
⊢ IsMultiplyPreprimitive G α 2

Tactic:
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]

Premises used: le_rfl, MulAction.is_one_preprimitive_iff, MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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})
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective

Premises used: MulAction.IsPreprimitive.of_surjective, Function.Bijective.surjective, SubMulAction.ofFixingSubgroup_of_singleton_bijective
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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})
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
exact IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective

Premises used: MulAction.IsPreprimitive.of_surjective
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}
h : 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)

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
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}
h :
  IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) → IsMultiplyPretransitive G α 2
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2

Tactic:
rw [hsa]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}
h :
  IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) →
    IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) → IsMultiplyPretransitive G α 2

Tactic:
rw [ofStabilizer.isMultiplyPretransitive (a := a)]

Premises used: SubMulAction.ofStabilizer.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}
h :
  IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G (α := α) {a}) ↥(ofFixingSubgroup G {a}) →
    IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
⊢ 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 [is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}) →
    IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
IsPretransitive.of_surjective_map
      ofFixingSubgroup_of_singleton_bijective.surjective

Premises used: Set.Mem, Function.Bijective.surjective, MulAction.IsPretransitive.of_surjective_map, SubMulAction.ofFixingSubgroup_of_singleton_bijective
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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}) →
    IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
exact IsPretransitive.of_surjective_map
      ofFixingSubgroup_of_singleton_bijective.surjective

Premises used: MulAction.IsPretransitive.of_surjective_map
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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)
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)
⊢ (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

Premises used: HMul.hMul, Nat.card, HAdd.hAdd, Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
hn1 : 2 * (n + 1) < Nat.card α
rwa rwa₁ rwa₂ rwa₃ : 1 < n + 1
⊢ 1 < s.ncard

Tactic:
rwa [hsn]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
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
hn1 : 2 * (n + 1) < Nat.card α
⊢ 1 < s.ncard

Tactic:
have : 1 < s.ncard := by rwa [hsn]