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 β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
grw : insert b s ⊆ Y
⊢ s ⊆ Y
have grw₁ : Y ⊆ Y
Tactic: grw [subset_insert b s, hsY]
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
have insert : ∀ (y1 : F) (hy1 : y1 ∈ Y) (hty1 : ∀ x ∈ X', t < f x y1), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic: obtain ⟨y1, hy1, hty1⟩ := hrec (by grw [subset_insert b s, hsY]) ht_lt
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
have insert : ∀ (x : E) (hx : x ∈ X), t < max (f x b) (f x y1)
Tactic: refine exists_lt_iInf_of_lt_iInf_of_sup ne_X kX hfy hfy' cY hfx hfx' hb hy1 fun 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 β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
⊢ t < max (f x b) (f x y1)
have pos : ∀ (hx' : x ∈ X'), t < max (f x b) (f x y1)
Tactic: by_cases hx' : x ∈ X'
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
pos : ∀ (hx' : x ∈ X'), t < max (f x b) (f x y1)
⊢ t < max (f x b) (f x y1)
have neg : ∀ (hx' : x ∉ X'), t < max (f x b) (f x y1)
Tactic: by_cases hx' : x ∈ X'
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∉ X'
⊢ t < max (f x b) (f x y1)
have apply : t < f x b
Tactic: apply lt_of_lt_of_le _ (le_sup_left)
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
s_1 : Set F
t : β
b : F
s : Set F
h : b ∉ s
hs : s.Finite
X : Set 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
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
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x b) ⁻¹' Iic t
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∉ X'
⊢ t < f x b
have rw : ¬f x b ≤ t
Tactic: rw [← not_le]
-- 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
⊢ inf_sup = sup_inf
have a : sup_inf = inf_sup
Tactic: apply symm
-- 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
⊢ sup_inf = inf_sup
have a : sup_inf ≤ inf_sup
Tactic: apply le_antisymm
-- 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
a : sup_inf ≤ inf_sup
⊢ sup_inf = inf_sup
have a₁ : inf_sup ≤ sup_inf
Tactic: apply le_antisymm
-- 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
⊢ sup_inf ≤ inf_sup
have a : ∀ (x : β), Membership.mem (γ := Set β) {x : β | ∃ x_1 ∈ X, sup_y x_1 = x} x → sup_inf ≤ x
Tactic: rw [le_isGLB_iff hinf_sup, mem_lowerBounds]
-- 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
x : E
hx : x ∈ X
⊢ sup_inf ≤ sup_y x
have a : ∀ (x_1 : β), Membership.mem (γ := Set β) {x : β | ∃ y ∈ Y, inf_x y = x} x_1 → x_1 ≤ sup_y x
Tactic: rw [isLUB_le_iff hsup_inf, mem_upperBounds]
-- 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
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ inf_x y ≤ sup_y x
have trans : inf_x y ≤ f x y
Tactic: trans f x y
-- 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
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
trans : inf_x y ≤ f x y
⊢ inf_x y ≤ sup_y x
have trans₁ : f x y ≤ sup_y x
Tactic: trans f x y
-- 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
⊢ inf_sup ≤ sup_inf
have a : ∀ (hfy : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X)
  (hfy' : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y)
  (cY : Convex.{0, u_2} ℝ (E := F) ∅) (hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) ∅)
  (hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) ∅ fun (y : F) ↦ f x y)
  (hsup_y : ∀ x ∈ X, IsLUB {x_1 : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ f x y = x_1} (sup_y x))
  (hinf_x : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → IsGLB {x : β | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y))
  (hsup_inf : IsLUB {x : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ inf_x y = x} sup_inf), inf_sup ≤ sup_inf
Tactic: rcases eq_empty_or_nonempty Y with ⟨rfl⟩ | ne_Y
Cleared hypotheses: Y, hfy, hfy', cY, hfx, hfx', hsup_y, hinf_x, hsup_inf
-- 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
a :
  ∀
    (hfy :
      ∀ (y : F), Membership.mem (γ := Set F) ∅ y → LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X)
    (hfy' : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y)
    (cY : Convex.{0, u_2} ℝ (E := F) ∅)
    (hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) ∅)
    (hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) ∅ fun (y : F) ↦ f x y)
    (hsup_y : ∀ x ∈ X, IsLUB {x_1 : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ f x y = x_1} (sup_y x))
    (hinf_x : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → IsGLB {x : β | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y))
    (hsup_inf : IsLUB {x : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ inf_x y = x} sup_inf), inf_sup ≤ sup_inf
⊢ inf_sup ≤ sup_inf
have a₁ : ∀ (ne_Y : Y.Nonempty), inf_sup ≤ sup_inf
Tactic: rcases eq_empty_or_nonempty Y with ⟨rfl⟩ | ne_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
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
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : DenselyOrdered β
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x : β | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
hfy : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
cY : Convex.{0, u_2} ℝ (E := F) ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) ∅ fun (y : F) ↦ f x y
hsup_y : ∀ x ∈ X, IsLUB {x_1 : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ f x y = x_1} (sup_y x)
hinf_x : ∀ (y : F), Membership.mem (γ := Set F) ∅ y → IsGLB {x : β | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
hsup_inf : IsLUB {x : β | ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ inf_x y = x} sup_inf
⊢ inf_sup ≤ sup_inf
have hfy₁ : True
Tactic: simp only [mem_empty_iff_false, IsEmpty.forall_iff, implies_true, false_and, exists_const,
      setOf_false, isLUB_empty_iff] at *
Cleared hypotheses: hfy, hfy', hsup_y, hinf_x, hsup_inf