internlm/Lean-Github huggingface dataset:
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
α : 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
⊢ g • {a} = {b}
Tactic:
change (fun x => g • x) '' {a} = {b}
Proof state after:
α : 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
⊢ (fun x => g • x) '' {a} = {b}
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
α : 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
⊢ (fun x => g • x) '' {a} = {b}
Tactic:
rw [Set.image_singleton, hg]
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 : ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
obtain ⟨a, t, _, hst⟩ := this
Proof state after:
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
have ha' : a ∉ Subtype.val '' t := by
  intro h; rw [Set.mem_image] at h ; obtain ⟨x, hx⟩ := h
  apply x.prop; rw [hx.right]; exact Set.mem_singleton a
Proof state after:
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
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
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
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
  rw [isPreprimitive_iff_is_one_preprimitive]
  rw [← stabilizer.isMultiplyPreprimitive G α (Nat.le_refl 1) hG.toIsPretransitive]
  apply is_two_preprimitive_weak_jordan hG hsn hα hGs
Proof state after:
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
  (SubMulAction.ofFixingSubgroup (stabilizer G a) t) :=  by
  apply isPreprimitive_of_surjective_map
    (SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective G a t).surjective
  apply isPreprimitive_of_surjective_map
    (SubMulAction.OfFixingSubgroupOfEq.map_bijective G hst).surjective
  exact hGs
Proof state after:
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
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)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))
Tactic:
rw [← Nat.succ_eq_one_add]
Proof state after:
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)
⊢ IsMultiplyPreprimitive G α (Nat.succ (Nat.succ (Nat.succ n)))
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)
⊢ a ∉ Subtype.val '' t
Tactic:
intro h
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)
h : a ∈ Subtype.val '' t
⊢ False
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)
h : a ∈ Subtype.val '' t
⊢ False
Tactic:
rw [Set.mem_image] at h
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)
h : ∃ x ∈ t, ↑x = a
⊢ False
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)
h : ∃ x ∈ t, ↑x = a
⊢ False
Tactic:
obtain ⟨x, hx⟩ := h
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ False
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ False
Tactic:
apply x.prop
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}
Tactic:
rw [hx.right]
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}
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 : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer G a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}
Tactic:
exact Set.mem_singleton a
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
⊢ IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
Tactic:
rw [isPreprimitive_iff_is_one_preprimitive]
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 (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1