Theorem: Partition.eq_empty (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition ⊥
⊢ P = Partition.empty α
Tactic:
ext x
State after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
⊢ x ∈ P ↔ x ∈ Partition.empty α

State before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
have hsup := P.sSup_eq
State after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : sSup ↑P = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α

State before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : sSup ↑P = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
simp only [sSup_eq_bot, SetLike.mem_coe] at hsup
State after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α

State before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
simp only [not_mem_empty, iff_false]
State after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∉ P

State before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∉ P
Tactic:
exact fun hx ↦ P.ne_bot_of_mem hx <| hsup x hx
State after:
no goals