obtain ⟨t', ⟨-, 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
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
⊢ t = 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
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
t' : Set α
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t = P.partOf x