Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro
β : 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
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
⊢ False
Tactic:
have hJ1J2 : J1 ∩ J2 = ∅ := by
  rw [Set.eq_empty_iff_forall_not_mem]
  simp only [mem_inter_iff, not_and]
  rintro ⟨z, hz⟩ hz1 hz2
  simp only [mem_J1_iff] at hz1
  simp only [mem_J2_iff] at hz2
  have hz_mem_Y : z ∈ Y := cY.segment_subset hy1 hy2 hz
  apply Set.Nonempty.not_subset_empty (nonempty_C X ne_X kX Y f hfy ⟨z, hz_mem_Y⟩ hinfi_le)
  rw [Set.subset_empty_iff, ← bot_eq_empty, ← disjoint_self]
  exact Set.disjoint_of_subset hz1 hz2 (disjoint_C X Y f a t' ⟨y1, hy1⟩ ⟨y2, hy2⟩ ha' ht')
Proof state after:
case intro.intro.intro.intro
β : 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
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : J1 ∩ J2 = ∅
⊢ False