have l_mono : Monotone l := by {
  intro a b hab
  have := h {a, b}
  rw [Sup_pair.1 hab, Set.image_pair] at this
  exact Sup_pair.2 this.symm
}
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 x ≤ 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