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
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
⊢ inf_sup = sup_inf

Tactic:
by
  apply symm
  apply le_antisymm
  -- the obvious inequality
  · rw [le_isGLB_iff hinf_sup, mem_lowerBounds]
    rintro _ ⟨x, hx, rfl⟩
    rw [isLUB_le_iff hsup_inf, mem_upperBounds]
    rintro _ ⟨y, hy, rfl⟩
    trans f x y
    · exact (hinf_x y hy).1 ⟨x, hx, rfl⟩
    · exact (hsup_y x hx).1 ⟨y, hy, rfl⟩
  -- the delicate inequality
  rcases eq_empty_or_nonempty Y with ⟨rfl⟩ | ne_Y
  · -- the case when `Y` is empty is trivial
    simp only [mem_empty_iff_false, IsEmpty.forall_iff, implies_true, false_and, exists_const,
      ofPred_false, isLUB_empty_iff] at *
    replace hsup_y : ∀ x ∈ X, sup_y x = sup_inf :=
      fun x hx ↦ le_antisymm (hsup_y x hx sup_inf) (hsup_inf (sup_y x))
    suffices {t | ∃ x ∈ X, sup_y x = t} = {sup_inf} from (this ▸ hinf_sup).unique (by simp) |>.le
    ext t
    simp only [mem_ofPred_eq, mem_singleton_iff]
    constructor
    · rintro ⟨x, hx, rfl⟩
      exact hsup_y x hx
    · rintro rfl
      exact ⟨_, ne_X.choose_spec, hsup_y _ ne_X.choose_spec⟩
  -- when `Y` is not empty
  rw [← forall_lt_iff_le]
  intro t ht
  have : ∃ s : Finset Y, ∀ x ∈ X, ∃ i ∈ s, t < f x i := by
    rw [← LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset kX hfy]
    apply Set.eq_empty_of_forall_notMem
    rintro x ⟨hx, hx'⟩
    simp only [mem_iInter, mem_preimage, mem_Iic] at hx'
    rw [lt_isGLB_iff hinf_sup] at ht
    obtain ⟨c, hc, htc⟩ := ht
    simp only [mem_lowerBounds, mem_ofPred_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hc
    apply not_le.mpr htc (le_trans (hc x hx) _)
    rw [isLUB_le_iff (hsup_y x hx), mem_upperBounds]
    aesop
  obtain ⟨s, hs⟩ := this
  have hs' (x) (hx : x ∈ X) : ∃ y ∈ Subtype.val '' (s : Set Y), t < f x y := by
    obtain ⟨i, hi, hi'⟩ := hs x hx
    use i.val
    simp [hi, hi']
  choose y0 hy0 ht0 using exists_lt_iInf_of_lt_iInf_of_finite
        ne_X kX hfy hfy' cY hfx hfx' cX
        (t := t)
        (toFinite _) (Subtype.coe_image_subset Y ↑s)
  simp only [lt_isLUB_iff hsup_inf, mem_ofPred_eq, exists_exists_and_eq_and]
  use y0 hs', hy0 hs'
  specialize ht0 hs'
  obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy (y0 hs') (hy0 hs'))
  apply lt_of_lt_of_le (ht0 a ha)
  simpa [le_isGLB_iff (hinf_x (y0 hs') (hy0 hs')), mem_lowerBounds]

Goal state after: