rw [symm_iff_of r, rel_iff_eqv_class_eq_right hx, eq_comm]
α : 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 α
hx : r x x
⊢ r x y ↔ {z | r x z} = {z | r y z}
no goals