intro z hzt'
case hp
β : 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
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✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
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
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, f a ↑y ⊔ f a ↑y' ≤ f x ↑y ⊔ f x ↑y'
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < f a ↑y ⊔ f a ↑y'
hbb' : b < b'
z : ↑(segment ℝ ↑y ↑y')
hz :
  ∃ᶠ (x : F) in nhdsWithin (↑z) Y,
    ∃ (h : x ∈ segment ℝ ↑y ↑y'), { val := x, property := h } ∈ ERealSion.J X Y f b b' y y'
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
this : f ↑x ↑z < b'
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
⊢ ∀ (x_1 : F),
    f (↑x) x_1 < b' →
      (∃ (hz' : x_1 ∈ segment ℝ ↑y ↑y'), { val := x_1, property := hz' } ∈ ERealSion.J X Y f b b' y y') →
        ∃ (hz' : x_1 ∈ segment ℝ ↑y ↑y'),
          x ∈ ERealSion.C X f b' x_1 ∧ { val := x_1, property := hz' } ∈ ERealSion.J X Y f b b' y y'
case hp
β : 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
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✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
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
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, f a ↑y ⊔ f a ↑y' ≤ f x ↑y ⊔ f x ↑y'
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < f a ↑y ⊔ f a ↑y'
hbb' : b < b'
z✝ : ↑(segment ℝ ↑y ↑y')
hz :
  ∃ᶠ (x : F) in nhdsWithin (↑z✝) Y,
    ∃ (h : x ∈ segment ℝ ↑y ↑y'), { val := x, property := h } ∈ ERealSion.J X Y f b b' y y'
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z✝
hzY : ↑z✝ ∈ Y
this : f ↑x ↑z✝ < b'
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z✝) Y, f (↑x) x' < b'
z : F
hzt' : f (↑x) z < b'
⊢ (∃ (hz' : z ∈ segment ℝ ↑y ↑y'), { val := z, property := hz' } ∈ ERealSion.J X Y f b b' y y') →
    ∃ (hz' : z ∈ segment ℝ ↑y ↑y'),
      x ∈ ERealSion.C X f b' z ∧ { val := z, property := hz' } ∈ ERealSion.J X Y f b b' y y'