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
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
apply : 1 ≤ t.ncard
⊢ t.ncard = t.ncard - 1 + 1

Tactic:
apply (Nat.sub_eq_iff_eq_add ?_).mp rfl

Premises used: Nat.sub_eq_iff_eq_add, Iff.mp, rfl
-- 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
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
rw : t.Nonempty
⊢ 1 ≤ t.ncard

Tactic:
rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, Set.ncard_pos]

Premises used: Nat.pos_iff_ne_zero, Set.ncard_pos, Nat.one_le_iff_ne_zero
-- 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
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
h' : Nat.card α ≤ s.ncard + (g • s).ncard
h : s ∪ g • s ≠ Set.univ
⊢ t.Nonempty

Tactic:
apply Set.nonempty_inter_of_le_ncard_add_ncard

Premises used: Set.nonempty_inter_of_le_ncard_add_ncard
-- 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
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
h' : Nat.card α ≤ 2 * (n + 1)
⊢ Nat.card α ≤ s.ncard + (g • s).ncard

Tactic:
rw [Set.ncard_smul_set, ← two_mul, hsn]

Premises used: two_mul, Set.ncard_smul_set
-- 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
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
⊢ Nat.card α ≤ 2 * (n + 1)

Tactic:
hn2
-- 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
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
⊢ Nat.card α ≤ 2 * (n + 1)

Tactic:
exact hn2
-- 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
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
h : s ∪ g • s = Set.univ
rw : Membership.mem (γ := Set α) Set.univ a
⊢ a ∈ s ∪ g • s

Tactic:
rw [h]
-- 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
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
h : s ∪ g • s = Set.univ
⊢ Membership.mem (γ := Set α) Set.univ a

Tactic:
trivial
-- 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
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
⊢ s ∪ g • s ≠ Set.univ

Tactic:
exact fun h ↦ ha (by rw [h]; trivial)
-- 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
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

Tactic:
have htm : t.ncard = t.ncard - 1 + 1 := by
      apply (Nat.sub_eq_iff_eq_add ?_).mp rfl
      rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, Set.ncard_pos]
      apply Set.nonempty_inter_of_le_ncard_add_ncard
      · rw [Set.ncard_smul_set, ← two_mul, hsn]; exact hn2
      · exact fun h ↦ ha (by rw [h]; trivial)
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
rw : t.ncard < s.ncard
⊢ t.ncard - 1 < n

Tactic:
rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]

Premises used: Nat.lt_iff_add_one_le, Nat.le_iff_lt_add_one
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
apply : t ⊂ s
⊢ t.ncard < s.ncard

Tactic:
apply Set.ncard_lt_ncard _

Premises used: Set.ncard_lt_ncard
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
⊢ t ⊂ s

Tactic:
⟨Set.inter_subset_left, fun h ↦ hb ?_⟩

Premises used: Set.inter_subset_left, 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 : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
refine : ∀ (h : s ⊆ t), b ∈ s
⊢ t ⊂ s

Tactic:
refine ⟨Set.inter_subset_left, fun h ↦ hb ?_⟩
-- 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_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
this : s = g • s
rw : b ∈ g • s
⊢ b ∈ s

Tactic:
rw [this]
-- 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_1 : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
this : s = g • s
⊢ b ∈ g • s

Tactic:
simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb

Premises used: Set.smul_set_compl, Set.not_notMem, Set.mem_compl_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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
suffices : s = g • s
⊢ b ∈ s

Tactic:
suffices s = g • s by
        rw [this]
        simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
apply : s ⊆ g • s
apply₁ : (g • s).ncard ≤ s.ncard
⊢ s = g • s

Tactic:
apply Set.eq_of_subset_of_ncard_le _ _ (g • s).toFinite

Premises used: Set.toFinite, Set.eq_of_subset_of_ncard_le, HSMul.hSMul
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
⊢ s ⊆ g • s

Tactic:
subset_trans h Set.inter_subset_right

Premises used: subset_trans, Set.inter_subset_right
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
⊢ s ⊆ g • s

Tactic:
exact subset_trans h Set.inter_subset_right

Premises used: subset_trans, Set.inter_subset_right
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
rw rw₁ : s.ncard ≤ s.ncard
⊢ (g • s).ncard ≤ s.ncard

Tactic:
rw [Set.ncard_smul_set]

Premises used: Set.ncard_smul_set
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard - 1 < n

Tactic:
have hmn : t.ncard - 1 < n := by
      rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]
      apply Set.ncard_lt_ncard _
      refine ⟨Set.inter_subset_left, fun h ↦ hb ?_⟩
      suffices s = g • s by
        rw [this]
        simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb
      apply Set.eq_of_subset_of_ncard_le _ _ (g • s).toFinite
      · exact subset_trans h Set.inter_subset_right
      · rw [Set.ncard_smul_set]
-- 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
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha_1 : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
⊢ t.ncard - 1 + 2 < Nat.card α

Tactic:
have htm' : t.ncard - 1 + 2 < Nat.card α := lt_trans (Nat.add_lt_add_right hmn 2) hsn'