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

State before:
X : Type u_1
inst✝ : PartialOrder X
s : Set X
x₀ : X
h : isInf s x₀
⊢ x₀ ∈ lowerBounds s
Tactic:
sorry
State after:
no goals