internlm/Lean-Github huggingface dataset:
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
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1
Tactic:
rw [← stabilizer.isMultiplyPreprimitive G α (Nat.le_refl 1) hG.toIsPretransitive]
Proof state after:
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
⊢ IsMultiplyPreprimitive G α (Nat.succ 1)
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
⊢ IsMultiplyPreprimitive G α (Nat.succ 1)
Tactic:
apply is_two_preprimitive_weak_jordan hG hsn hα hGs
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)
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
Tactic:
apply isPreprimitive_of_surjective_map
  (SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective G a t).surjective
Proof state after:
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)
⊢ IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
    ↥(SubMulAction.ofFixingSubgroup G (insert a (Subtype.val '' t)))
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)
⊢ IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
    ↥(SubMulAction.ofFixingSubgroup G (insert a (Subtype.val '' t)))
Tactic:
apply isPreprimitive_of_surjective_map
  (SubMulAction.OfFixingSubgroupOfEq.map_bijective G hst).surjective
Proof state after:
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)
⊢ IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
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)
⊢ IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
Tactic:
exact hGs
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_1
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
⊢ Set.ncard t = Nat.succ n
Tactic:
rw [← Set.ncard_image_of_injective t Subtype.val_injective]
Proof state after:
case refine'_1
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
⊢ Set.ncard (Subtype.val '' t) = Nat.succ n
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_1.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 : α
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
⊢ Set.ncard (Subtype.val '' t) + ?refine'_1.m = Nat.succ n + ?refine'_1.m

case refine'_1.m
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
⊢ ℕ
Tactic:
rw [← Set.ncard_insert_of_not_mem ha', ← hst, hsn]
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2
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 n < Fintype.card ↥(SubMulAction.ofStabilizer G a)
Tactic:
change _ < Fintype.card (SubMulAction.ofStabilizer G a).carrier
Proof state after:
case refine'_2
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 n < Fintype.card ↑(SubMulAction.ofStabilizer G a).carrier
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2
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 n < Fintype.card ↑(SubMulAction.ofStabilizer G a).carrier
Tactic:
rw [← Nat.card_eq_fintype_card, Set.Nat.card_coe_set_eq]
Proof state after:
case refine'_2
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 n < Set.ncard (SubMulAction.ofStabilizer G a).carrier
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2
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 n < Set.ncard (SubMulAction.ofStabilizer G a).carrier
Tactic:
rw [SubMulAction.ofStabilizer_carrier]
Proof state after:
case refine'_2
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 n < Set.ncard {a}ᶜ
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2
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 n < Set.ncard {a}ᶜ
Tactic:
rw [← Nat.succ_eq_one_add]
Proof state after:
case refine'_2
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
⊢ Nat.succ (Nat.succ n) < Set.ncard {a}ᶜ
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
⊢ Set.ncard {a} + Nat.succ (Nat.succ n) < Nat.card α
Tactic:
simp only [Set.ncard_singleton, Nat.card_eq_fintype_card]
Proof state after:
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 α