refine (f.rel_apply ha).trans ?_
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel a b
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel (f a) b