rw [Set.pair_comm x x']
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x, x'} = x'
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x', x} = x'