Theorem: ERealSion.isClosed_J (Sion/Sion.lean)

State before:
β : 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, 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
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'
⊢ IsClosed (ERealSion.J X Y f b b' y y')
Tactic:
rw [isClosed_iff_clusterPt]
State after:
β : 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, 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
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'
⊢ ∀ (a : ↑(segment ℝ ↑y ↑y')),
    ClusterPt a (Filter.principal (ERealSion.J X Y f b b' y y')) → a ∈ ERealSion.J X Y f b b' y y'

State before:
β : 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, 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
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'
⊢ ∀ (a : ↑(segment ℝ ↑y ↑y')),
    ClusterPt a (Filter.principal (ERealSion.J X Y f b b' y y')) → a ∈ ERealSion.J X Y f b b' y y'
Tactic:
intro z hz x hx
State after:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
⊢ x ∈ ERealSion.C X f b' ↑y

State before:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
⊢ x ∈ ERealSion.C X f b' ↑y
Tactic:
have hzY :=(convex_iff_segment_subset.mp cY) y.prop y'.prop z.prop
State after:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ x ∈ ERealSion.C X f b' ↑y

State before:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ x ∈ ERealSion.C X f b' ↑y
Tactic:
suffices ∃ z' ∈ J X Y f b b' y y', x ∈ C X f b' (z' : F) by
  obtain ⟨z', hz', hxz'⟩ := this
  suffices C X f b' z' ⊆ C X f b' y by
    exact this hxz'
  apply Or.resolve_right (C_subset_or X Y cY f hfx' hfy hfy' a b' y y' ha hb' z')
  intro hz'2
  have hz'Y :=(convex_iff_segment_subset.mp cY) y.prop y'.prop z'.prop
  apply (nonempty_C X ne_X kX Y f hfy ⟨z', hz'Y⟩ hb).not_subset_empty
  simp only [← disjoint_iff_inter_eq_empty.mp (disjoint_C X Y f a b' y y' ha hb')]
  apply Set.subset_inter hz'
  apply subset_trans (monotone_C X Y f b b' ⟨z', hz'Y⟩ hbb'.le) hz'2
State after:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
simp only [UpperSemicontinuousOn, UpperSemicontinuousWithinAt] at hfx
State after:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
have := lt_of_le_of_lt hx hbb'
State after:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
this : ((fun x => f x ↑z) ∘ fun x => ↑x) x < b'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
this : ((fun x => f x ↑z) ∘ fun x => ↑x) x < b'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
dsimp only [Function.comp_apply] at this
State after:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (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'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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, ∀ x_1 ∈ Y, ∀ (y : β), f x x_1 < y → ∀ᶠ (x' : F) in nhdsWithin x_1 Y, f x x' < 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
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 : ClusterPt z (Filter.principal (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'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
specialize hfx x.val x.prop z (cY.segment_subset y.prop y'.prop z.prop) b'
  (lt_of_le_of_lt hx hbb')
State after:
β : 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 : ClusterPt z (Filter.principal (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' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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 : ClusterPt z (Filter.principal (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' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
rw [Filter.clusterPt_principal_subtype_iff_frequently (cY.segment_subset y.prop y'.prop)] at hz
State after:
β : 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' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
β : 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' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
suffices ∀ᶠ z' : F in nhdsWithin z Y,
  (∃ hz' : z' ∈ segment ℝ y.val y'.val, (⟨z', hz'⟩ : segment ℝ y.val y'.val) ∈ J X Y f b b' y y') →
    ∃ hz' : z' ∈ segment ℝ y.val y'.val, x ∈ C X f b' z'
      ∧ (⟨z', hz'⟩ : segment ℝ y.val y'.val) ∈ J X Y f b b' y y' by
  obtain ⟨z', hz', hxz'1, hxz'2⟩ := Filter.Frequently.exists (Filter.Frequently.mp hz this)
  exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩
State after:
β : 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) in nhdsWithin (↑z) Y,
    (∃ (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'

State before:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
this : ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
⊢ x ∈ ERealSion.C X f b' ↑y
Tactic:
obtain ⟨z', hz', hxz'⟩ := this
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ x ∈ ERealSion.C X f b' ↑y

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ x ∈ ERealSion.C X f b' ↑y
Tactic:
suffices C X f b' z' ⊆ C X f b' y by
  exact this hxz'
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y
Tactic:
apply Or.resolve_right (C_subset_or X Y cY f hfx' hfy hfy' a b' y y' ha hb' z')
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ ¬ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
⊢ ¬ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
Tactic:
intro hz'2
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
⊢ False

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
⊢ False
Tactic:
have hz'Y :=(convex_iff_segment_subset.mp cY) y.prop y'.prop z'.prop
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ False

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ False
Tactic:
apply (nonempty_C X ne_X kX Y f hfy ⟨z', hz'Y⟩ hb).not_subset_empty
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑{ val := ↑z', property := hz'Y } ⊆ ∅

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑{ val := ↑z', property := hz'Y } ⊆ ∅
Tactic:
simp only [← disjoint_iff_inter_eq_empty.mp (disjoint_C X Y f a b' y y' ha hb')]
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑z' ⊆ ERealSion.C X f b' ↑y ∩ ERealSion.C X f b' ↑y'

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑z' ⊆ ERealSion.C X f b' ↑y ∩ ERealSion.C X f b' ↑y'
Tactic:
apply Set.subset_inter hz'
State after:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑z' ⊆ ERealSion.C X f b' ↑y'

State before:
case intro.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
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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
hz'2 : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ ERealSion.C X f b ↑z' ⊆ ERealSion.C X f b' ↑y'
Tactic:
apply subset_trans (monotone_C X Y f b b' ⟨z', hz'Y⟩ hbb'.le) hz'2
State after:
no goals

State before:
β : 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, 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
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 : ClusterPt z (Filter.principal (ERealSion.J X Y f b b' y y'))
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hzY : ↑z ∈ Y
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ ERealSion.J X Y f b b' y y'
hxz' : x ∈ ERealSion.C X f b' ↑z'
this : ERealSion.C X f b' ↑z' ⊆ ERealSion.C X f b' ↑y
⊢ x ∈ ERealSion.C X f b' ↑y
Tactic:
exact this hxz'
State after:
no goals

State before:
β : 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'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (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'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
obtain ⟨z', hz', hxz'1, hxz'2⟩ := Filter.Frequently.exists (Filter.Frequently.mp hz this)
State after:
case intro.intro.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
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'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (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'
z' : F
hz' : z' ∈ segment ℝ ↑y ↑y'
hxz'1 : x ∈ ERealSion.C X f b' z'
hxz'2 : { val := z', property := hz' } ∈ ERealSion.J X Y f b b' y y'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'

State before:
case intro.intro.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
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'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (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'
z' : F
hz' : z' ∈ segment ℝ ↑y ↑y'
hxz'1 : x ∈ ERealSion.C X f b' z'
hxz'2 : { val := z', property := hz' } ∈ ERealSion.J X Y f b b' y y'
⊢ ∃ z' ∈ ERealSion.J X Y f b b' y y', x ∈ ERealSion.C X f b' ↑z'
Tactic:
exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩
State after:
no goals

State before:
β : 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) in nhdsWithin (↑z) Y,
    (∃ (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'
Tactic:
apply Filter.Eventually.mp hfx
State after:
β : 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) in nhdsWithin (↑z) Y,
    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'

State before:
β : 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) in nhdsWithin (↑z) Y,
    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'
Tactic:
apply Filter.eventually_of_forall
State after:
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'

State before:
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'
Tactic:
intro z hzt'
State after:
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'

State before:
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'
Tactic:
rintro ⟨hz, hz'⟩
State after:
case hp.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
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'
hz' : { 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'

State before:
case hp.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
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'
hz' : { 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'
Tactic:
exact ⟨hz, ⟨le_of_lt hzt', hz'⟩⟩
State after:
no goals