internlm/Lean-Github huggingface dataset:
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton B
Tactic:
rw [hB']
Proof state after:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton ↑⊥
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton ↑⊥
Tactic:
exact Set.subsingleton_singleton
Proof state after:
no goals
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ IsTrivialBlock B
Tactic:
right
Proof state after:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ B = ⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ B = ⊤
Tactic:
rw [hB']
Proof state after:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = ⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: maximal_stabilizer_iff_preprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ Subgroup.IsMaximal (stabilizer G a) ↔ IsPreprimitive G X
Tactic:
rw [isPreprimitive_iff_isSimpleOrder_blocks G a, Subgroup.isMaximal_def, ← Set.isSimpleOrder_Ici_iff_isCoatom]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Theorem: maximal_stabilizer_iff_preprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
simp only [isSimpleOrder_iff_isCoatom_bot]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥
Theorem: maximal_stabilizer_iff_preprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥
Tactic:
rw [← OrderIso.isCoatom_iff (stabilizerBlockEquiv G a), OrderIso.map_bot]
Proof state after:
no goals
Theorem: hasMaximalStabilizersOfPreprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
⊢ Subgroup.IsMaximal (stabilizer G a)
Tactic:
haveI : IsPretransitive G X := hpGX.toIsPretransitive
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ Subgroup.IsMaximal (stabilizer G a)
Theorem: hasMaximalStabilizersOfPreprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ Subgroup.IsMaximal (stabilizer G a)
Tactic:
rw [maximal_stabilizer_iff_preprimitive]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Theorem: hasMaximalStabilizersOfPreprimitive
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Tactic:
exact hpGX
Proof state after:
no goals
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ Nontrivial α
Tactic:
apply Or.resolve_left (subsingleton_or_nontrivial α)
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ ¬Subsingleton α
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ ¬Subsingleton α
Tactic:
intro hα
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ False
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ False
Tactic:
apply h
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ fixedPoints (↥N) α = ⊤
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ fixedPoints (↥N) α = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ ⊤ ≤ fixedPoints (↥N) α
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ ⊤ ≤ fixedPoints (↥N) α
Tactic:
intro x hx
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ x ∈ fixedPoints (↥N) α
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ x ∈ fixedPoints (↥N) α
Tactic:
rw [mem_fixedPoints]
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ ∀ (m : ↥N), m • x = x
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ ∀ (m : ↥N), m • x = x
Tactic:
intro g
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Tactic:
rw [subsingleton_iff] at hα
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : ∀ (x y : α), x = y
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Theorem: isnontrivial_of_nontrivial_action
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : ∀ (x y : α), x = y
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Tactic:
apply hα
Proof state after:
no goals
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
⊢ IsQuasipreprimitive M α
Tactic:
apply IsQuasipreprimitive.mk
Proof state after:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
⊢ ∀ {N : Subgroup M}, Subgroup.Normal N → fixedPoints (↥N) α ≠ ⊤ → IsPretransitive (↥N) α
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
⊢ ∀ {N : Subgroup M}, Subgroup.Normal N → fixedPoints (↥N) α ≠ ⊤ → IsPretransitive (↥N) α
Tactic:
intro N hN hNX
Proof state after:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
⊢ IsPretransitive (↥N) α
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
⊢ IsPretransitive (↥N) α
Tactic:
have : ∃ x : α, x ∉ fixedPoints N α :=
  by
  rw [← Set.ne_univ_iff_exists_not_mem, ← Set.top_eq_univ]
  exact hNX
Proof state after:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
this : ∃ x, x ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
this : ∃ x, x ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Tactic:
obtain ⟨a, ha⟩ := this
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Tactic:
rw [← MulAction.orbit.isPretransitive_iff a]
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ orbit (↥N) a = ⊤
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ orbit (↥N) a = ⊤
Tactic:
apply Or.resolve_left (hGX.has_trivial_blocks (orbit.IsBlock_of_normal hN a))
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ ¬Set.Subsingleton (orbit (↥N) a)
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ ¬Set.Subsingleton (orbit (↥N) a)
Tactic:
intro h
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ False
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ False
Tactic:
apply ha
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ a ∈ fixedPoints (↥N) α
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ a ∈ fixedPoints (↥N) α
Tactic:
simp only [mem_fixedPoints]
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ ∀ (m : ↥N), m • a = a
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
⊢ ∀ (m : ↥N), m • a = a
Tactic:
intro n
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ n • a = a
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ n • a = a
Tactic:
rw [← Set.mem_singleton_iff]
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ n • a ∈ {a}
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ n • a ∈ {a}
Tactic:
suffices orbit N a = {a} by rw [← this]; use n
Proof state after:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ orbit (↥N) a = {a}
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
⊢ ∃ x, x ∉ fixedPoints (↥N) α
Tactic:
rw [← Set.ne_univ_iff_exists_not_mem, ← Set.top_eq_univ]
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
⊢ fixedPoints (↥N) α ≠ ⊤
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
⊢ fixedPoints (↥N) α ≠ ⊤
Tactic:
exact hNX
Proof state after:
no goals
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ {a}
Tactic:
rw [← this]
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ orbit (↥N) a
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ orbit (↥N) a
Tactic:
use n
Proof state after:
no goals
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
⊢ orbit (↥N) a = {a}
Tactic:
ext b
Proof state after:
case pretransitive_of_normal.intro.h
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
b : α
⊢ b ∈ orbit (↥N) a ↔ b ∈ {a}
Theorem: IsPreprimitive.isQuasipreprimitive
Proof state before:
case pretransitive_of_normal.intro.h
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
N : Subgroup M
hN : Subgroup.Normal N
hNX : fixedPoints (↥N) α ≠ ⊤
a : α
ha : a ∉ fixedPoints (↥N) α
h : Set.Subsingleton (orbit (↥N) a)
n : ↥N
b : α
⊢ b ∈ orbit (↥N) a ↔ b ∈ {a}
Tactic:
rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]
Proof state after:
no goals
Theorem: isPreprimitive_of_prime
Proof state before:
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Theorem: isPreprimitive_of_prime
Proof state before:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_prime
Proof state before:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
cases' Set.subsingleton_or_nontrivial B with hB' hB'
Proof state after:
case has_trivial_blocks'.inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ IsTrivialBlock B

case has_trivial_blocks'.inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_prime
Proof state before:
case has_trivial_blocks'.inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
Proof state after:
case has_trivial_blocks'.inl.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ Set.Subsingleton B
Theorem: isPreprimitive_of_prime
Proof state before:
case has_trivial_blocks'.inl.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ Set.Subsingleton B
Tactic:
exact hB'
Proof state after:
no goals