rw [eq_comm, f.apply_eq_apply_iff_rel ha]
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f (f a) = f a
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ P.Rel a (f a)