internlm/Lean-Github huggingface dataset:
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case succ
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_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ (Nat.succ n) →
          1 + Nat.succ (Nat.succ n) < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
intro α G _ _ _ hG s hsn hα hGs
Proof state after:
case succ
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case succ
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)
⊢ Set.Nonempty s
Tactic:
rw [← Set.ncard_pos, hsn]
Proof state after:
case succ
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)
⊢ 0 < Nat.succ (Nat.succ n)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case succ
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)
⊢ 0 < Nat.succ (Nat.succ n)
Tactic:
apply Nat.succ_pos
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero

⊢ ∀ {α : 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 Nat.zero →
          1 + Nat.succ Nat.zero < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
intro α G _ _ _ hG s hsn _ hGs
Proof state after:
case zero
α : 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.zero
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero
α : 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.zero
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
haveI : IsPretransitive G α := hG.toIsPretransitive
Proof state after:
case zero
α : 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.zero
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero
α : 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.zero
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
simp only [Set.ncard_eq_one] at hsn
Proof state after:
case zero
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
hsn : ∃ a, s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
hsn : ∃ a, s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
obtain ⟨a, hsa⟩ := hsn
Proof state after:
case zero.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
a : α
hsa : s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
this : IsPretransitive G α
a : α
hsa : s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
rw [hsa] at hGs
Proof state after:
case zero.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)
Tactic:
constructor
Proof state after:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPretransitive G α (1 + Nat.succ Nat.zero)

case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(1 + Nat.succ Nat.zero) →
      IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPretransitive G α (1 + Nat.succ Nat.zero)
Tactic:
rw [stabilizer.isMultiplyPretransitive]
Proof state after:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPretransitive (↥(stabilizer G ?zero.intro.left.a)) (↥(SubMulAction.ofStabilizer G ?zero.intro.left.a)) 1

case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPretransitive (↥(stabilizer G ?zero.intro.left.a)) (↥(SubMulAction.ofStabilizer G ?zero.intro.left.a)) 1

case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α
Tactic:
rw [← isPretransitive_iff_is_one_pretransitive]
Proof state after:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive ↥(stabilizer G ?zero.intro.left.a) ↥(SubMulAction.ofStabilizer G ?zero.intro.left.a)

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α

case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.left
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive ↥(stabilizer G ?zero.intro.left.a) ↥(SubMulAction.ofStabilizer G ?zero.intro.left.a)

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α

case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α

case zero.intro.left.a
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α
Tactic:
apply isPretransitive.of_surjective_map
  (SubMulAction.OfFixingSubgroupOfSingleton.map_bijective G a).surjective
  hGs.toIsPretransitive
Proof state after:
case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.left.hα'
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive G α
Tactic:
exact hG.toIsPretransitive
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(1 + Nat.succ Nat.zero) →
      IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
Tactic:
intro t h
Proof state after:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t + 1 = ↑(1 + Nat.succ Nat.zero)
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t + 1 = ↑(1 + Nat.succ Nat.zero)
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
simp only [Nat.zero_eq, Nat.cast_add, Nat.cast_one] at h
Proof state after:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t + 1 = 1 + 1
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t + 1 = 1 + 1
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
rw [← Nat.cast_one, WithTop.add_eq_add_iff, Nat.cast_one] at h
Proof state after:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
obtain ⟨b, htb⟩ := Set.encard_eq_one.mp h
Proof state after:
case zero.intro.right.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G a b
Proof state after:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
have hst : g • ({a} : Set α) = ({b} : Set α) := by
  change (fun x => g • x) '' {a} = {b}
  rw [Set.image_singleton, hg]
Proof state after:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
hst : g • {a} = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
hst : g • {a} = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
Tactic:
rw [htb]
Proof state after:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
hst : g • {a} = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G {b}) ↥(SubMulAction.ofFixingSubgroup G {b})
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case zero.intro.right.intro.intro
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn'✝ : 1 + Nat.succ Nat.zero < Fintype.card α
this : IsPretransitive G α
a : α
hGs : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
t : Set α
h : Set.encard t = 1
b : α
htb : t = {b}
g : G
hg : g • a = b
hst : g • {a} = {b}
⊢ IsPreprimitive ↥(fixingSubgroup G {b}) ↥(SubMulAction.ofFixingSubgroup G {b})
Tactic:
refine' isPreprimitive_of_surjective_map
  (SubMulAction.conjMap_ofFixingSubgroup_bijective G hst).surjective hGs
Proof state after:
no goals