internlm/Lean-Github huggingface dataset:
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2.a
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
this : n + 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ (Nat.succ n) < Fintype.card α
Tactic:
exact hα
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case intro.intro.intro
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ n + 2 = 1 + Nat.succ n
Tactic:
exact Nat.succ_eq_one_add (n + 1)
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ 1 ≤ n + 2
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ 0 ≤ n + 1
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case a
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ 0 ≤ n + 1
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : Set.Nonempty s
⊢ ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
Tactic:
obtain ⟨a, ha⟩ := this
Proof state after:
case intro
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case intro
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
Tactic:
use a
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ ∃ t, a ∈ s ∧ s = insert a (Subtype.val '' t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ ∃ t, a ∈ s ∧ s = insert a (Subtype.val '' t)
Tactic:
use Subtype.val ⁻¹' s
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ a ∈ s ∧ s = insert a (Subtype.val '' (Subtype.val ⁻¹' s))
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ a ∈ s ∧ s = insert a (Subtype.val '' (Subtype.val ⁻¹' s))
Tactic:
apply And.intro ha
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (Subtype.val '' (Subtype.val ⁻¹' s))
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (Subtype.val '' (Subtype.val ⁻¹' s))
Tactic:
rw [Set.image_preimage_eq_inter_range]
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ Set.range Subtype.val)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ Set.range Subtype.val)
Tactic:
rw [Set.insert_eq]
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = {a} ∪ s ∩ Set.range Subtype.val
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = {a} ∪ s ∩ Set.range Subtype.val
Tactic:
simp only [Subtype.range_coe_subtype, Set.singleton_union, Set.mem_inter_iff, Set.mem_setOf_eq]
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | x ∈ SubMulAction.ofStabilizer G a})
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | x ∈ SubMulAction.ofStabilizer G a})
Tactic:
simp_rw [SubMulAction.mem_ofStabilizer_iff]
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | x ≠ a})
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | x ≠ a})
Tactic:
simp only [Ne.def]
Proof state after:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | ¬x = a})
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
⊢ s = insert a (s ∩ {x | ¬x = a})
Tactic:
ext x
Proof state after:
case h.h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔ x ∈ insert a (s ∩ {x | ¬x = a})
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case h.h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔ x ∈ insert a (s ∩ {x | ¬x = a})
Tactic:
rw [Set.mem_insert_iff]
Proof state after:
case h.h
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔ x = a ∨ x ∈ s ∩ {x | ¬x = a}