rw [minimax X ne_X cX kX Y cY f hfx hfx' hfy hfy']
case right
β : Type u_3
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
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
hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X
a : E
ha : a ∈ X
ha' : ⨆ y ∈ Y, f a y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
b : F
hb : b ∈ Y
hb' : ⨅ x ∈ X, f x b = ⨆ x ∈ Y, ⨅ x_1 ∈ X, f x_1 x
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨅ x ∈ X, f x b
case right
β : Type u_3
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
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
hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X
a : E
ha : a ∈ X
ha' : ⨆ y ∈ Y, f a y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
b : F
hb : b ∈ Y
hb' : ⨅ x ∈ X, f x b = ⨆ x ∈ Y, ⨅ x_1 ∈ X, f x_1 x
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, f x b