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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
a :
  ∀ (y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F)
    (hy0 :
      ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y),
        y0 ht ∈ Y)
    (ht0 :
      ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y),
        ∀ x ∈ X, t < f x (y0 ht)),
    t < sup_inf
⊢ t < sup_inf

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

Premises used: Subtype.coe_image_subset, Set.toFinite, SetLike.coe, Sion.exists_lt_iInf_of_lt_iInf_of_finite
-- 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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 :
  ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y),
    ∀ x ∈ X, t < f x (y0 ht)
a : ∃ a ∈ Y, t < inf_x a
⊢ t < sup_inf

Tactic:
simp only [lt_isLUB_iff hsup_inf, mem_setOf_eq, exists_exists_and_eq_and]

Premises used: lt_isLUB_iff, Set.mem_setOf_eq, exists_exists_and_eq_and
-- 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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 :
  ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y),
    ∀ x ∈ X, t < f x (y0 ht)
right : t < inf_x (y0 hs')
⊢ ∃ a ∈ Y, t < inf_x a

Tactic:
use y0 hs', hy0 hs'
-- 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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 :
  ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y),
    ∀ x ∈ X, t < f x (y0 ht)
⊢ ∀ x ∈ X, t < f x (y0 hs')

Tactic:
specialize ht0 hs'
-- 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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 : ∀ x ∈ X, t < f x (y0 hs')
right : ∀ (a : E) (ha : a ∈ X) (h : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (y0 hs')) X a), t < inf_x (y0 hs')
⊢ t < inf_x (y0 hs')

Tactic:
obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy (y0 hs') (hy0 hs'))

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- 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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 : ∀ x ∈ X, t < f x (y0 hs')
a : E
ha : a ∈ X
h : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (y0 hs')) X a
right : f a (y0 hs') ≤ inf_x (y0 hs')
⊢ t < inf_x (y0 hs')

Tactic:
apply lt_of_lt_of_le (ht0 a ha)

Premises used: lt_of_lt_of_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
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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
s : Finset (↑Y : Type u_2)
hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
hs' : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
y0 : (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y) → F
hy0 : ∀ (ht : ∀ x ∈ X, ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y), y0 ht ∈ Y
ht0 : ∀ x ∈ X, t < f x (y0 hs')
a : E
ha : a ∈ X
h : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (y0 hs')) X a
⊢ f a (y0 hs') ≤ inf_x (y0 hs')

Tactic:
simpa [le_isGLB_iff (hinf_x (y0 hs') (hy0 hs')), mem_lowerBounds]

Premises used: mem_lowerBounds, le_isGLB_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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
⊢ ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Y, IsMaxOn (f x) Y y

Tactic:
have hmax_y (x) (hx : x ∈ X) : ∃ y ∈ Y, IsMaxOn (f x) Y y := (hfx x hx).exists_isMaxOn ne_Y kY
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
hmax_y : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Y, IsMaxOn (f x) Y y
choose! :
  ∀ (η : (x : E) → F) (η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y) (η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)),
    ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
choose! η η_mem η_max using hmax_y
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
⊢ LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X

Tactic:
have hlsc : LowerSemicontinuousOn (fun x => f x (η x)) X :=
    lowerSemicontinuousOn_of_forall_isMaxOn_and_mem hfy η_mem η_max
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
⊢ ∃ a ∈ X, IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a

Tactic:
hlsc.exists_isMinOn ne_X kX

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
obtain :
  ∀ (a : E) (ha : a ∈ X) (ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a),
    ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨a, ha, ha'⟩ : ∃ a ∈ X, IsMinOn (fun x ↦ f x (η x)) X a := hlsc.exists_isMinOn ne_X kX

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a
right : ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a
⊢ ∀ (y : F) (hy : y ∈ Y), ∃ x ∈ X, IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x

Tactic:
have hmin_x (y) (hy : y ∈ Y) : ∃ x ∈ X, IsMinOn (f · y) X x := (hfy y hy).exists_isMinOn ne_X kX
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a
hmin_x : ∀ (y : F) (hy : y ∈ Y), ∃ x ∈ X, IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x
right :
  ∀ (ξ : (y : F) → E) (ξ_mem : ∀ (y : F) (hy : y ∈ Y), ξ y ∈ X)
    (ξ_min : ∀ (y : F) (hy : y ∈ Y), IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X (ξ y)),
    ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
choose! ξ ξ_mem ξ_min using hmin_x
-- 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
kY : IsCompact 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
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : (x : E) → F
η_mem : ∀ (x : E) (hx : x ∈ X), η x ∈ Y
η_max : ∀ (x : E) (hx : x ∈ X), IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (η x)) X a
ξ : (y : F) → E
ξ_mem : ∀ (y : F) (hy : y ∈ Y), ξ y ∈ X
ξ_min : ∀ (y : F) (hy : y ∈ Y), IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X (ξ y)
⊢ UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y

Tactic:
have husc := upperSemicontinuousOn_of_forall_isMinOn_and_mem hfx ξ_mem ξ_min