awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
this : ∃ (s : Finset (↑Y : Type u_2)), ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
⊢ t < sup_inf
have a : ∀ (s : Finset (↑Y : Type u_2)) (hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)), t < sup_inf
Tactic: obtain ⟨s, hs⟩ := this
Cleared hypotheses: this
-- 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
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)
x : E
hx : x ∈ X
⊢ ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
have obtain : ∀ (i : (↑Y : Type u_2)) (hi : i ∈ s) (hi' : t < f x (↑i : F)),
  ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
Tactic: obtain ⟨i, hi, hi'⟩ := hs x hx
-- 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
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)
x : E
hx : x ∈ X
i : (↑Y : Type u_2)
hi : i ∈ s
hi' : t < f x (↑i : F)
⊢ ∃ y ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)), t < f x y
have h : (↑i : F) ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)) ∧ t < f x (↑i : F)
Tactic: use i.val
-- 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
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)
⊢ t < sup_inf
have 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
Tactic: have hs' (x) (hx : x ∈ X) : ∃ y ∈ Subtype.val '' (s : Set Y), t < f x y := by
    obtain ⟨i, hi, hi'⟩ := hs x hx
    use i.val
    simp [hi, hi']
-- 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
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
⊢ t < sup_inf
have 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
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)
-- 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
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)
⊢ t < sup_inf
have a : ∃ a ∈ Y, t < inf_x a
Tactic: simp only [lt_isLUB_iff hsup_inf, mem_setOf_eq, exists_exists_and_eq_and]
-- 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
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 ∈ Y, t < inf_x a
have right : t < inf_x (y0 hs')
Tactic: use y0 hs', hy0 hs'
-- 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
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)
⊢ t < inf_x (y0 hs')
have ht0₁ : ∀ x ∈ X, t < f x (y0 hs')
Tactic: specialize ht0 hs'
Cleared hypotheses: ht0
-- 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
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')
⊢ t < inf_x (y0 hs')
have 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')
Tactic: obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy (y0 hs') (hy0 hs'))
-- 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
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
⊢ t < inf_x (y0 hs')
have right : f a (y0 hs') ≤ inf_x (y0 hs')
Tactic: apply lt_of_lt_of_le (ht0 a ha)
-- 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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hmax_y : ∀ (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
-- 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
hmax_y : ∀ (x : E) (hx : x ∈ X), ∃ y ∈ Y, IsMaxOn (f x) Y y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have 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
Tactic: choose! η η_mem η_max using hmax_y
Cleared hypotheses: hmax_y
-- 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)
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hlsc : 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
-- 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 ∈ 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) ↦ f x (η x)) X a),
  ∃ 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
-- 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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have right : ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic: use a, ha