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

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