rw [h t ⟨ht, hxt⟩, h (P.partOf x) ⟨P.partOf_mem hx, P.mem_partOf hx⟩]
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
no goals