Theorem: Tutorial.isInf.lowerBound (GlimpseOfLean/Solutions/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:
rw [h]
State after:
no goals