Theorem: Tutorial.adjunction_of_Sup (GlimpseOfLean/Exercises/Topics/GaloisAdjunctions.lean)

State before:
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)
⊢ adjunction l (mk_right l)
Tactic:
sorry
State after:
no goals