awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hmin_x : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have 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
Tactic: choose! ξ ξ_mem ξ_min using hmin_x
Cleared hypotheses: hmin_x
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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)
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (x : F) ↦ f (ξ x) x) Y
Tactic: have husc := upperSemicontinuousOn_of_forall_isMinOn_and_mem hfx ξ_mem ξ_min
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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, IsSaddlePointOn X Y f a b
have 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
Tactic: obtain ⟨b, hb, hb'⟩ : ∃ b ∈ Y, IsMaxOn (fun y ↦ f (ξ y) y) Y b := husc.exists_isMaxOn ne_Y kY
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have right : IsSaddlePointOn X Y f a b
Tactic: use b, hb
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ SemicontinuousWithinAt (fun (x1 : E) (x2 : β) ↦ (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) x1 > x2) X x
have h : ∀ (i : F), LowerSemicontinuousWithinAt.{u_1, u_3} (β := β) (fun (x1 : E) ↦ ⨆ (_ : i ∈ Y), f x1 i) X x
Tactic: apply lowerSemicontinuousWithinAt_iSup
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hlsc : 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
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ SemicontinuousWithinAt (fun (x1 : F) (x2 : β) ↦ (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) x1 < x2) Y y
have h : ∀ (i : E), UpperSemicontinuousWithinAt.{u_2, u_3} (β := β) (fun (x1 : F) ↦ ⨅ (_ : i ∈ X), f i x1) Y y
Tactic: apply upperSemicontinuousWithinAt_iInf
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have husc : 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
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have 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
Tactic: obtain ⟨a, ha, ha'⟩ := LowerSemicontinuousOn.exists_isMinOn
   ne_X kX hlsc
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have 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
Tactic: obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_isMaxOn ne_Y kY husc
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have right : IsSaddlePointOn X Y f a b
Tactic: use a, ha, b, hb
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ IsSaddlePointOn X Y f a b
have right : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
Tactic: rw [isSaddlePointOn_iff' ha hb]
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
have right : LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨅ x ∈ X, f x b)
Tactic: refine le_trans (le_iInf₂ ha') ?_
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨅ x ∈ X, f x b)
have right : LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨆ i ∈ Y, (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) i)
Tactic: refine le_trans ?_ (iSup₂_le_iff.mpr hb')
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i)
    (⨆ i ∈ Y, (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) i)
have right : LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)
Tactic: rw [minimax' ne_X cX kX hfy hfy' cY hfx hfx']
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
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_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : 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
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
Tactic: have hφx (x) (hx : x ∈ X) : UpperSemicontinuousOn (fun y ↦ φ x y) Y := by
    convert! Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone