refine ⟨fun ⟨t, htP, hxt, hyt⟩ ↦ ?_, fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, ?_⟩⟩
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
⊢ P.Rel x y ↔ P.partOf x = P.partOf y
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ P.partOf x = P.partOf y

case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
h : P.partOf x = P.partOf y
⊢ y ∈ P.partOf x