apply (CompleteLattice.I_isInf _).eq
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ Inf {x, x'} = x
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ isInf {x, x'} x