apply le_iSup₂ y hy
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ ⨆ y ∈ Y, f a y
no goals