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 : AddCommGroup F
inst_2 : Module ℝ F
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
hfx' :
  Convex.{0, u_2} ℝ (E := F)
    {x_1 : F | x_1 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_1}
⊢ ∀ ⦃x_1 : F⦄,
    Membership.mem (γ := Set F)
        {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2} x_1 →
      ∀ ⦃y_1 : F⦄,
        Membership.mem (γ := Set F)
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
            y_1 →
          segment ℝ x_1 y_1 ⊆
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}

Tactic:
rw [convex_iff_segment_subset] at hfx'

Premises used: convex_iff_segment_subset
-- 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 : AddCommGroup F
inst_2 : Module ℝ F
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
hfx' :
  ∀ ⦃x_1 : F⦄,
    Membership.mem (γ := Set F)
        {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2} x_1 →
      ∀ ⦃y_1 : F⦄,
        Membership.mem (γ := Set F)
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
            y_1 →
          segment ℝ x_1 y_1 ⊆
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
⊢ Membership.mem (γ := Set F)
    {x_1 : F | x_1 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_1} (↑z : F)

Tactic:
specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop

Premises used: inf_le_right, Subtype.prop, And.intro, inf_le_left
-- 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 : AddCommGroup F
inst_2 : Module ℝ F
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
hfx' :
  Membership.mem (γ := Set F)
    {x_1 : F | x_1 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_1} (↑z : F)
⊢ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b

Tactic:
le_trans hfx'.2 hx

Premises used: And.right, le_trans
-- 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 : AddCommGroup F
inst_2 : Module ℝ F
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
hfx' :
  Membership.mem (γ := Set F)
    {x_1 : F | x_1 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_1} (↑z : F)
⊢ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b

Tactic:
exact le_trans hfx'.2 hx

Premises used: And.right, le_trans
-- 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 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : AddCommGroup F
inst_7 : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
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
cY : Convex ℝ Y
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
apply :
  sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) (↑z : F) ⋯) : F) ∩
      (sublevelLeft X f b (↑y : F) ∩ sublevelLeft X f b (↑y' : F)) =
    ∅
⊢ sublevelLeft X f b (↑z : F) ⊆ sublevelLeft X f b (↑y : F) ∨ sublevelLeft X f b (↑z : F) ⊆ sublevelLeft X f b (↑y' : F)

Tactic:
apply isPreconnected_iff_subset_of_disjoint_closed.mp
    (isPreconnected_sublevelLeft hfy' b ⟨z, cY.segment_subset y.prop y'.prop z.prop⟩)
    _ _ (isClosed_sublevelLeft hfy b y) (isClosed_sublevelLeft hfy b y')
    (sublevelLeft_subset_union hfx' b y y' z)

Premises used: _private.0.Sion.sublevelLeft_subset_union, isPreconnected_iff_subset_of_disjoint_closed, _private.0.Sion.isClosed_sublevelLeft, Subtype.mk, Subtype.prop, _private.0.Sion.isPreconnected_sublevelLeft, Iff.mp, Subtype.val, Convex.segment_subset
-- 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 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : AddCommGroup F
inst_7 : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
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
cY : Convex ℝ Y
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
⊢ sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) (↑z : F) ⋯) : F) ∩
      (sublevelLeft X f b (↑y : F) ∩ sublevelLeft X f b (↑y' : F)) =
    ∅

Tactic:
simp [(disjoint_sublevelLeft ha hb).inter_eq]

Premises used: _private.0.Sion.disjoint_sublevelLeft, Disjoint.inter_eq
-- 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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
by_contra! : ∀ (hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t), False
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
by_contra! hinfi_le
-- 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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
obtain : ∀ (a : E) (ha : a ∈ X) (ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x y1) (f x y2)) X a), False
⊢ False

Tactic:
obtain ⟨a, ha, ha'⟩ := (hfy y1 hy1).sup (hfy y2 hy2) |>.exists_isMinOn ne_X kX

Premises used: LowerSemicontinuousOn.exists_isMinOn, LowerSemicontinuousOn.sup
-- 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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x y1) (f x y2)) X a
obtain : ∀ (t' : β) (htt' : t < t') (ht' : t' < max (f a y1) (f a y2)), False
⊢ False

Tactic:
obtain ⟨t', htt', ht'⟩ := exists_between (ht a ha)

Premises used: exists_between
-- 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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x y1) (f x y2)) X a
t' : β
htt' : t < t'
ht' : t' < max (f a y1) (f a y2)
⊢ y1 ∈ Y

Tactic:
hy1
-- 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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < max (f x y1) (f x y2)
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x y1) (f x y2)) X a
t' : β
htt' : t < t'
ht' : t' < max (f a y1) (f a y2)
lift :
  ∀ (y1 : { x : F // x ∈ Y }) (ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x y2))
    (ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x y2)) X a)
    (ht' : t' < max (f a (↑y1 : F)) (f a y2)), False
⊢ False

Tactic:
lift y1 to Y using hy1
-- 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
y2 : F
hy2 : y2 ∈ Y
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x y2)
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x y2)) X a
ht' : t' < max (f a (↑y1 : F)) (f a y2)
⊢ y2 ∈ Y

Tactic:
hy2
-- 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
y2 : F
hy2 : y2 ∈ Y
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x y2)
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x y2)) X a
ht' : t' < max (f a (↑y1 : F)) (f a y2)
lift :
  ∀ (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))), False
⊢ False

Tactic:
lift y2 to Y using hy2
-- 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
z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)
⊢ z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)

Tactic:
simp [J1, setOf_sublevelLeft_subset]

Premises used: _private.0.Sion.setOf_sublevelLeft_subset
-- 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
⊢ ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)

Tactic:
have mem_J1_iff (z : segment ℝ (y1 : F) y2) :
      z ∈ J1 ↔ sublevelLeft X f t z ⊆ sublevelLeft X f t' y1 := by
    simp [J1, setOf_sublevelLeft_subset]
-- 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)
z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)
⊢ z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)

Tactic:
simp [J2, setOf_sublevelLeft_subset, φ, Homeomorph.setCongr]

Premises used: _private.0.Sion.setOf_sublevelLeft_subset, Homeomorph.setCongr
-- 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)
⊢ ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)

Tactic:
have mem_J2_iff (z : segment ℝ (y1 : F) y2) :
      z ∈ J2 ↔ sublevelLeft X f t z ⊆ sublevelLeft X f t' y2 := by
    simp [J2, setOf_sublevelLeft_subset, φ, Homeomorph.setCongr]
-- 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)
⊢ ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y

Tactic:
have h_mem_Y (z : segment ℝ (y1 : F) y2) : (z : F) ∈ Y := cY.segment_subset y1.2 y2.2 z.prop