calc
  l x ≤ l (mk_right l y) := l_mono h'
  _   = Sup (l '' { x | l x ≤ y }) := h {x | l x ≤ y}
  _   ≤ Sup { y' | y' ≤ y } := Sup_subset (Set.image_preimage_subset l { y' | y' ≤ y })
  _   = y := Sup_le_self y
case mpr
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
l_mono : Monotone l
⊢ l x ≤ y
no goals