intro hz
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ∈ lowerBounds {x, x'} → z ≤ x
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ z ≤ x