exact Sup_pair.2 this.symm
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l b = Sup {l a, l b}
⊢ l a ≤ l b
no goals