exact (CompleteLattice.S_isSup {x | l x ≤ y}).upperBound h'
case mp
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' : l x ≤ y
⊢ x ≤ mk_right l y
no goals