Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
by_contra! hinfi_le
  obtain ⟨a, ha, ha'⟩ := (hfy y1 hy1).sup (hfy y2 hy2) |>.exists_isMinOn ne_X kX
  obtain ⟨t', htt', ht'⟩ := exists_between (ht a ha)
  lift y1 to Y using hy1
  lift y2 to Y using hy2
  let J1 := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
  have mem_J1_iff (z : segment ℝ (y1 : F) y2) :
      z ∈ J1 ↔ sublevelLeft X f t z ⊆ sublevelLeft X f t' y1 := by
    simp [J1, setOfPred_sublevelLeft_subset]
  let φ : segment ℝ (y1 : F) y2 ≃ₜ segment ℝ (y2 : F) y1 := .setCongr (segment_symm ℝ (y1 : F) y2)
  let J2 := φ ⁻¹' (setOfPred_sublevelLeft_subset X Y f t t' y2 y1)
  have mem_J2_iff (z : segment ℝ (y1 : F) y2) :
      z ∈ J2 ↔ sublevelLeft X f t z ⊆ sublevelLeft X f t' y2 := by
    simp [J2, setOfPred_sublevelLeft_subset, φ, Homeomorph.setCongr]
  have h_mem_Y (z : segment ℝ (y1 : F) y2) : (z : F) ∈ Y := cY.segment_subset y1.2 y2.2 z.prop
  have hJ1J2 : J1 ∩ J2 = ∅ := by
    rw [Set.eq_empty_iff_forall_notMem]
    simp only [mem_inter_iff, mem_J1_iff, mem_J2_iff]
    intro z ⟨hz1, hz2⟩
    apply (nonempty_sublevelLeft ne_X kX hfy ⟨z, h_mem_Y z⟩ hinfi_le).not_subset_empty
    simpa using Set.disjoint_of_subset hz1 hz2 (disjoint_sublevelLeft ha' ht')
  have hJ1_union_J2 : J1 ∪ J2 = segment ℝ (y1 : F) y2 := by
    refine subset_antisymm (by simp) fun z hz ↦ ?_
    lift z to segment ℝ (y1 : F) y2 using hz
    refine ⟨z, ?_, rfl⟩
    apply sublevelLeft_subset_or hfx' hfy hfy' cY a t' y1 y2 ha' ht' z |>.imp
      (fun h1 ↦ ?_) (fun h2 ↦ ?_)
    · grw [mem_J1_iff, (monotone_sublevelLeft ⟨(z : F), h_mem_Y z⟩ htt'.le), h1]
    · grw [mem_J2_iff, (monotone_sublevelLeft ⟨(z : F), h_mem_Y z⟩ htt'.le), h2]
  have : IsPreconnected (Set.univ : Set (segment ℝ (y1 : F) y2)) := by
    simpa [← Topology.IsInducing.subtypeVal.isPreconnected_image] using
      (convex_segment (y1 : F) y2).isPreconnected
  have hJ1 : IsClosed J1 := isClosed_setOfPred_sublevelLeft_subset ne_X kX hfy hfy'
    cY hfx hfx' a t t' y1 y2 ha' hinfi_le ht' htt'
  have hJ2 : IsClosed J2 := by
    simp only [sup_comm (f _ y1)] at ha' ht'
    simpa [J2, sup_comm] using isClosed_setOfPred_sublevelLeft_subset ne_X kX hfy hfy'
      cY hfx hfx' a t t' y2 y1 ha' hinfi_le ht' htt'
  have h_univ : univ ⊆ J1 ∪ J2 :=
    image_subset_image_iff Subtype.val_injective |>.mp <| by simp [hJ1_union_J2]
  have h_inter : univ ∩ (J1 ∩ J2) = ∅ := by simp [hJ1J2]
  rw [isPreconnected_iff_subset_of_disjoint_closed] at this
  rw [eq_empty_iff_forall_notMem] at hJ1J2
  obtain (h1 | h2) := this J1 J2 hJ1 hJ2 h_univ h_inter
  · refine hJ1J2 ⟨y2, right_mem_segment ℝ (y1 : F) y2⟩ ⟨h1 (Set.mem_univ _), ?_⟩
    grw [mem_J2_iff, monotone_sublevelLeft y2 htt'.le]
  · refine hJ1J2 ⟨y1, left_mem_segment ℝ (y1 : F) y2⟩ ⟨?_, h2 (Set.mem_univ _)⟩
    grw [mem_J1_iff, monotone_sublevelLeft y1 htt'.le]

Goal state after: