Theorem: IsPreprimitive.isQuasipreprimitive (Jordan/Primitive.lean)

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
hGX : IsPreprimitive M α
⊢ IsQuasipreprimitive M α
Tactic:
apply IsQuasipreprimitive.mk
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) α

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
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) α

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
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) α

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
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) α

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]
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 = ⊤

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))
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)

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
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

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
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) α

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]
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

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
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

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]
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}

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
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}

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]
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) α ≠ ⊤

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
State after:
no goals

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]
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

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
State after:
no goals

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
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}

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)]
State after:
no goals