calc
  y ≤ I (upperBounds s) := (h _ y).mp (fun z hz ↦ hz hy)
  _ ≤ x                 := hx
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : (fun s => I (upperBounds s)) s ≤ x
y : X
hy : y ∈ s
⊢ y ≤ x
no goals