Theorem: IsPreprimitive.mk' (Jordan/Primitive.lean)

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X
Tactic:
have : ∃ a : X, a ∉ fixedPoints G X := by
  by_contra h; push_neg at h ; apply Hnt; rw [eq_top_iff]
  intro a _; exact h a
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
this : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
this : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Tactic:
obtain ⟨a, ha⟩ := this
State after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ IsPreprimitive G X

State before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk_mem' a ha
State after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B

State before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Tactic:
intro B _
State after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
B : Set X
x✝ : a ∈ B
⊢ IsBlock G B → IsTrivialBlock B

State before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
B : Set X
x✝ : a ∈ B
⊢ IsBlock G B → IsTrivialBlock B
Tactic:
exact H B
State after:
no goals

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
⊢ ∃ a, a ∉ fixedPoints G X
Tactic:
by_contra h
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ¬∃ a, a ∉ fixedPoints G X
⊢ False

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ¬∃ a, a ∉ fixedPoints G X
⊢ False
Tactic:
push_neg at h
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ False

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ False
Tactic:
apply Hnt
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ fixedPoints G X = ⊤

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ fixedPoints G X = ⊤
Tactic:
rw [eq_top_iff]
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ ⊤ ≤ fixedPoints G X

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ ⊤ ≤ fixedPoints G X
Tactic:
intro a _
State after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
a : X
a✝ : a ∈ ⊤
⊢ a ∈ fixedPoints G X

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
a : X
a✝ : a ∈ ⊤
⊢ a ∈ fixedPoints G X
Tactic:
exact h a
State after:
no goals