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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isSup S (⋃₀ S)
Tactic:
sorry
State after:
no goals