simp only [false_and, exists_const, imp_false, empty_subset, forall_true_left]
case refine'_1.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
s : Set F
hs : Set.Finite s
t : β
X : Set E
ne_X : Set.Nonempty X
cX✝ : Convex ℝ X
kX✝ : IsCompact X
hfx✝ : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx'✝ : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy✝ : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy'✝ : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
x : E
hx : x ∈ X
⊢ (∀ x ∈ X, ∃ y, False ∧ t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
case refine'_1.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
s : Set F
hs : Set.Finite s
t : β
X : Set E
ne_X : Set.Nonempty X
cX✝ : Convex ℝ X
kX✝ : IsCompact X
hfx✝ : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx'✝ : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy✝ : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy'✝ : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
x : E
hx : x ∈ X
⊢ (∀ (x : E), x ∉ X) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0