apply (CompleteLattice.I_isInf s _).1
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ≤ Inf s
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s