intros hx y hy
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s
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