intro x'
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ isInf {x' | x ≤ x'} x
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x