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
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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
⊢ ∃ b ∈ Y, IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b

Tactic:
husc.exists_isMaxOn ne_Y kY

Premises used: UpperSemicontinuousOn.exists_isMaxOn
-- 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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
right :
  ∀ (b : F) (hb : b ∈ Y) (hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b),
    ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨b, hb, hb'⟩ : ∃ b ∈ Y, IsMaxOn (fun y ↦ f (ξ y) y) Y b := husc.exists_isMaxOn ne_Y kY

Premises used: UpperSemicontinuousOn.exists_isMaxOn
-- 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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b
right : IsSaddlePointOn X Y f a b
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use b, hb
-- 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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f a (η a)

Tactic:
isMaxOn_iff.mp (η_max a ha) y hy

Premises used: isMaxOn_iff, Iff.mp
-- 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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f (ξ b) b ≤ f x b

Tactic:
isMinOn_iff.mp (ξ_min b hb) x hx

Premises used: Iff.mp, isMinOn_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) → 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)
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f (ξ y) y) Y b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b

Tactic:
calc f a y ≤ f a (η a) := isMaxOn_iff.mp (η_max a ha) y hy
    _ = f (ξ b) b :=
      minimax ne_X kX hfy hfy' cY hfx hfx' cX
        _ (fun x hx ↦ (η_max x hx).isLUB (η_mem x hx))
        _ (ha'.isGLB ha)
        _ (fun y hy ↦ (ξ_min y hy).isGLB (ξ_mem y hy))
        _ (hb'.isLUB hb)
    _ ≤ f x b := isMinOn_iff.mp (ξ_min b hb) x hx

Premises used: IsMinOn.isGLB, IsMaxOn.isLUB, isMaxOn_iff, Sion.minimax, Iff.mp, isMinOn_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ 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
⊢ Eq.{u_3 + 1} (α := β) (⨅ x ∈ X, ⨆ y ∈ Y, f x y) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)

Tactic:
minimax ne_X kX hfy hfy' cY hfx hfx' cX
   _ (fun _ _ ↦ isLUB_biSup) _ isGLB_biInf _ (fun _ _ ↦ isGLB_biInf) _ isLUB_biSup

Premises used: isGLB_biInf, Sion.minimax, isLUB_biSup
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
x : E
hx : x ∈ X
h : ∀ (i : F), LowerSemicontinuousWithinAt.{u_1, u_3} (β := β) (fun (x1 : E) ↦ ⨆ (_ : i ∈ Y), f x1 i) X x
⊢ SemicontinuousWithinAt (fun (x1 : E) (x2 : β) ↦ (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) x1 > x2) X x

Tactic:
apply lowerSemicontinuousWithinAt_iSup

Premises used: lowerSemicontinuousWithinAt_iSup
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
x : E
hx : x ∈ X
i : F
⊢ LowerSemicontinuousWithinAt.{u_1, u_3} (β := β) (fun (x1 : E) ↦ ⨆ (_ : i ∈ Y), f x1 i) X x

Tactic:
lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx

Premises used: lowerSemicontinuousWithinAt_iSup
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
x : E
hx : x ∈ X
i : F
⊢ LowerSemicontinuousWithinAt.{u_1, u_3} (β := β) (fun (x1 : E) ↦ ⨆ (_ : i ∈ Y), f x1 i) X x

Tactic:
exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx

Premises used: lowerSemicontinuousWithinAt_iSup
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
⊢ LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X

Tactic:
have hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X := fun x hx ↦ by
    apply lowerSemicontinuousWithinAt_iSup
    intro i
    exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
y : F
hy : y ∈ Y
h : ∀ (i : E), UpperSemicontinuousWithinAt.{u_2, u_3} (β := β) (fun (x1 : F) ↦ ⨅ (_ : i ∈ X), f i x1) Y y
⊢ SemicontinuousWithinAt (fun (x1 : F) (x2 : β) ↦ (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) x1 < x2) Y y

Tactic:
apply upperSemicontinuousWithinAt_iInf

Premises used: upperSemicontinuousWithinAt_iInf
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
y : F
hy : y ∈ Y
i : E
⊢ UpperSemicontinuousWithinAt.{u_2, u_3} (β := β) (fun (x1 : F) ↦ ⨅ (_ : i ∈ X), f i x1) Y y

Tactic:
upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy

Premises used: upperSemicontinuousWithinAt_iInf
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
y : F
hy : y ∈ Y
i : E
⊢ UpperSemicontinuousWithinAt.{u_2, u_3} (β := β) (fun (x1 : F) ↦ ⨅ (_ : i ∈ X), f i x1) Y y

Tactic:
exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy

Premises used: upperSemicontinuousWithinAt_iInf
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
⊢ UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y

Tactic:
have husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y := fun y hy ↦ by
    apply upperSemicontinuousWithinAt_iInf
    intro i
    exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
obtain :
  ∀ (a : E) (ha : a ∈ X) (ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) 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'⟩ := LowerSemicontinuousOn.exists_isMinOn
   ne_X kX hlsc

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
obtain :
  ∀ (b : F) (hb : b ∈ Y) (hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b),
    ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_isMaxOn ne_Y kY husc

Premises used: UpperSemicontinuousOn.exists_isMaxOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
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
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
right : IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha, b, hb