Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
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'
hX'X : X' ⊆ X
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
have kX' : IsCompact X' := by
  suffices X' = Subtype.val '' (Subtype.val ⁻¹' X' : Set X) by
    rw [this, ← Inducing.isCompact_iff inducing_subtype_val]
    haveI kX' : CompactSpace X := isCompact_iff_compactSpace.mp kX
    apply IsClosed.isCompact
    rw [inducing_subtype_val.isClosed_iff]
    specialize hfy b hb
    rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfy
    obtain ⟨v, hv, hv'⟩ := hfy t
    use v, hv
    rw [Subtype.preimage_coe_eq_preimage_coe_iff, ← hv']
    ext x
    simp only [mem_inter_iff, mem_preimage, mem_Iic, mem_setOf_eq, and_self_left, X']
  simp only [Set.image_preimage_eq_inter_range, ge_iff_le,
    Subtype.range_coe_subtype, setOf_mem_eq,
    Set.inter_eq_self_of_subset_left hX'X]
Proof state after:
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'
hX'X : X' ⊆ X
kX' : IsCompact X'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0