Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2
β : 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
hrec :
  ∀ (X : Set E),
    Set.Nonempty X →
      Convex ℝ X →
        IsCompact X →
          (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
            (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
              (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                  (∀ x ∈ X, ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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}
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
cases' Set.eq_empty_or_nonempty X' with X'_e X'_ne
Proof state after:
case refine'_2.inl
β : 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
hrec :
  ∀ (X : Set E),
    Set.Nonempty X →
      Convex ℝ X →
        IsCompact X →
          (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
            (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
              (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                  (∀ x ∈ X, ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'_e : X' = ∅
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

case refine'_2.inr
β : 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
hrec :
  ∀ (X : Set E),
    Set.Nonempty X →
      Convex ℝ X →
        IsCompact X →
          (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
            (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
              (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                  (∀ x ∈ X, ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0