awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
rw : ∀ (x : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), x ∉ J1 ∩ J2
⊢ J1 ∩ J2 = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
simp :
  ∀ (x : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    ¬(sublevelLeft X f t (↑x : F) ⊆ sublevelLeft X f t' (↑y1 : F) ∧
        sublevelLeft X f t (↑x : F) ⊆ sublevelLeft X f t' (↑y2 : F))
⊢ ∀ (x : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), x ∉ J1 ∩ J2

Tactic:
simp only [mem_inter_iff, mem_J1_iff, mem_J2_iff]

Premises used: Set.mem_inter_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)
this :
  ∀ (hz1 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F))
    (hz2 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)), False
⊢ ¬(sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F) ∧
      sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F))

Tactic:
⟨hz1, hz2⟩
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)
hz1 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
hz2 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
apply : sublevelLeft X f t (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) (↑z : F) ⋯) : F) ⊆ ∅
⊢ False

Tactic:
apply (nonempty_sublevelLeft ne_X kX hfy ⟨z, h_mem_Y z⟩ hinfi_le).not_subset_empty

Premises used: _private.0.Sion.nonempty_sublevelLeft, Subtype.mk, Subtype.val, Set.Nonempty.not_subset_empty
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)
hz1 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
hz2 : sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
⊢ sublevelLeft X f t (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) (↑z : F) ⋯) : F) ⊆ ∅

Tactic:
simpa using Set.disjoint_of_subset hz1 hz2 (disjoint_sublevelLeft ha' ht')

Premises used: Set.disjoint_of_subset, _private.0.Sion.disjoint_sublevelLeft
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
⊢ J1 ∩ J2 = ∅

Tactic:
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')
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
⊢ Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2) ⊆ segment ℝ (↑y1 : F) (↑y2 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
refine :
  ∀ (z : F) (hz : z ∈ segment ℝ (↑y1 : F) (↑y2 : F)),
    z ∈ Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2)
⊢ Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2) = segment ℝ (↑y1 : F) (↑y2 : F)

Tactic:
refine subset_antisymm (by simp) fun z hz ↦ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : F
hz : z ∈ segment ℝ (↑y1 : F) (↑y2 : F)
⊢ z ∈ segment ℝ (↑y1 : F) (↑y2 : F)

Tactic:
hz
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : F
hz : z ∈ segment ℝ (↑y1 : F) (↑y2 : F)
lift :
  ∀ (z : { x : F // x ∈ segment ℝ (↑y1 : F) (↑y2 : F) }),
    (↑z : F) ∈ Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2)
⊢ z ∈ Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2)

Tactic:
lift z to segment ℝ (y1 : F) y2 using hz

Premises used: Real, segment, Subtype.val