intro h x'' hx''
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ≤ x
x'' : X
hx'' : x'' ∈ {x' | x ≤ x'}
⊢ x' ≤ x''