apply lowerBound_Inf
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ Inf {x, x'} ≤ x'
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x' ∈ {x, x'}