Theorem: Block.mem_is_nontrivial_order_of_nontrivial (Jordan/Primitive.lean)

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ Nontrivial { B // a ∈ B ∧ IsBlock G B }
Tactic:
rw [nontrivial_iff]
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y
Tactic:
use (Block.boundedOrderOfMem G a).bot
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ y, ⊥ ≠ y

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ y, ⊥ ≠ y
Tactic:
use (Block.boundedOrderOfMem G a).top
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ⊥ ≠ ⊤

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ⊥ ≠ ⊤
Tactic:
intro h
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False
Tactic:
rw [← Subtype.coe_inj] at h
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
Tactic:
simp only [Block.boundedOrderOfMem.top_eq, Block.boundedOrderOfMem.bot_eq] at h
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
⊢ False

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
⊢ False
Tactic:
obtain ⟨b, hb⟩ := exists_ne a
State after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ False

State before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ False
Tactic:
apply hb
State after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b = a

State before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b = a
Tactic:
rw [← Set.mem_singleton_iff]
State after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ {a}

State before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ {a}
Tactic:
rw [h]
State after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ ⊤

State before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ ⊤
Tactic:
rw [Set.top_eq_univ]
State after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ Set.univ

State before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ Set.univ
Tactic:
apply Set.mem_univ
State after:
no goals