Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2.inr.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
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 : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
⊢ t < f x b ⊔ f x y1
Tactic:
by_cases hx' : x ∈ X'
Proof state after:
case pos
β : 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 : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∈ X'
⊢ t < f x b ⊔ f x y1

case neg
β : 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 : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∉ X'
⊢ t < f x b ⊔ f x y1