obtain ⟨_, ⟨h, -⟩⟩ := P.exists_unique_of_mem_set hx
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ x ∈ P.partOf x
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
w✝ : Set α
h : w✝ ∈ P ∧ x ∈ w✝
⊢ x ∈ P.partOf x