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
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ ↑y1 ↑y2
this : IsPreconnected univ
hJ1 : IsClosed J1
⊢ False

Tactic:
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'

Goal state after:
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
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ ↑y1 ↑y2
this : IsPreconnected univ
hJ1 : IsClosed J1
hJ2 : IsClosed J2
⊢ False