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

State before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
⊢ isSupFun fun s => I (upperBounds s)
Tactic:
sorry
State after:
no goals