intro x hx
case mp.right.a
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 : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ X, f a b ≤ f i b
case mp.right.a
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 : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b