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
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Tactic: suffices IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) →
      IsMultiplyPretransitive G α 2 by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      have ht_prim : IsPreprimitive (fixingSubgroup G t) (ofFixingSubgroup G t) := by
        apply IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter hs_prim
        apply Set.union_ne_univ_of_ncard_add_ncard_lt
        rwa [Set.ncard_smul_set, hsn, ← two_mul]
      apply (hrec (t.ncard - 1) hmn hG htm htm').2 ht_prim
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : 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 α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s ∪ g • s ≠ ⊤
have h : s.ncard + (g • s).ncard < Nat.card α
Tactic: apply Set.union_ne_univ_of_ncard_add_ncard_lt
-- 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
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s.ncard + (g • s).ncard < Nat.card α
have h : s.ncard + s.ncard < Nat.card α
Tactic: rwa [Set.ncard_smul_set, hsn, ← two_mul]
-- 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
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
h : s.ncard + s.ncard < Nat.card α
⊢ s.ncard + (g • s).ncard < Nat.card α
have h₁ : n + 1 + (n + 1) < Nat.card α
Tactic: rwa [Set.ncard_smul_set, hsn, ← two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2
have ht_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)
Tactic: have ht_trans : IsPretransitive (fixingSubgroup G t) (ofFixingSubgroup G t) :=
      IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs_trans (by
        apply Set.union_ne_univ_of_ncard_add_ncard_lt
        rwa [Set.ncard_smul_set, hsn, ← two_mul])
-- 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
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
ht_trans : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)
⊢ t.ncard - 1 + 2 < Nat.card α
have apply : t.ncard - 1 + 2 < n + 2
Tactic: apply lt_trans _ hsn'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
⊢ sᶜ.Nontrivial
have rwa : 1 < sᶜ.encard
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
⊢ sᶜ.Nontrivial
have rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
⊢ sᶜ.Nontrivial
have rwa₂ : 1 < sᶜ.ncard
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
rwa₂ : 1 < sᶜ.ncard
⊢ sᶜ.Nontrivial
have rwa₃ : s.ncard + 1 < s.ncard + sᶜ.ncard
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
rwa₂ : 1 < sᶜ.ncard
rwa₃ : s.ncard + 1 < s.ncard + sᶜ.ncard
rwa₄ : ℕ
⊢ sᶜ.Nontrivial
have rwa₅ : s.ncard + 1 < Nat.card α
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
rwa₂ : 1 < sᶜ.ncard
rwa₃ : s.ncard + 1 < s.ncard + sᶜ.ncard
rwa₄ : ℕ
rwa₅ : s.ncard + 1 < Nat.card α
⊢ sᶜ.Nontrivial
have rwa₆ : 1 + s.ncard < Nat.card α
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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 α
rwa : 1 < sᶜ.encard
rwa₁ : LT.lt (α := ℕ∞) 1 (↑sᶜ.ncard : ℕ∞)
rwa₂ : 1 < sᶜ.ncard
rwa₃ : s.ncard + 1 < s.ncard + sᶜ.ncard
rwa₄ : ℕ
rwa₅ : s.ncard + 1 < Nat.card α
rwa₆ : 1 + s.ncard < Nat.card α
⊢ sᶜ.Nontrivial
have rwa₇ : 1 + (n + 1) < Nat.card α
Tactic: rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
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)
have this₁ : sᶜ.Nontrivial
Tactic: have : Set.Nontrivial sᶜ := by
      rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]
-- 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_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
this : sᶜ.Nontrivial
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : ∀ (a : α) (ha : a ∈ sᶜ) (b : α) (hb : b ∈ sᶜ) (hab : a ≠ b),
  (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, ha : a ∈ sᶜ, b, hb : b ∈ sᶜ, hab⟩ := this
Cleared hypotheses: this
-- 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 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have h : ∀ (g : G) (hga : a ∈ g • sᶜ) (hgb : b ∉ g • sᶜ),
  (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 ⟨g, hga, hgb⟩ := exists_mem_smul_and_notMem_smul (G := G)
      sᶜ.toFinite (Set.nonempty_of_mem ha)
      (by simpa [Set.nonempty_iff_ne_empty] using hs_nonempty)
      hab
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
⊢ a ∉ s ∪ g • s
have hga₁ : a ∉ g • s
Tactic: simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha
Cleared hypotheses: ha, hga
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
hga₁ : a ∉ g • s
⊢ a ∉ s ∪ g • s
have ha₁ : a ∉ s
Tactic: simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha
Cleared hypotheses: ha, hga
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
⊢ (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
have ha₁ : a ∉ s ∪ g • s
Tactic: have ha : a ∉ s ∪ g • s := by
      simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha
      simp [ha, hga]
-- 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
⊢ t.ncard = t.ncard - 1 + 1
have apply : 1 ≤ t.ncard
Tactic: apply (Nat.sub_eq_iff_eq_add ?_).mp rfl