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
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
hfy₁ hfy'₁ : True
⊢ inf_sup ≤ sup_inf
have hsup_y₁ : ∀ x ∈ X, IsBot (sup_y x)
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
-- 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
hfy₁ hfy'₁ : True
hsup_y₁ : ∀ x ∈ X, IsBot (sup_y x)
hinf_x₁ : True
⊢ inf_sup ≤ sup_inf
have hsup_inf₁ : IsBot sup_inf
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
-- 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 : β
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
hfy hfy' : True
hsup_y : ∀ x ∈ X, IsBot (sup_y x)
hinf_x : True
hsup_inf : IsBot sup_inf
⊢ inf_sup ≤ sup_inf
have hsup_y₁ : ∀ x ∈ X, sup_y x = sup_inf
Tactic: replace hsup_y : ∀ x ∈ X, sup_y x = sup_inf :=
      fun x hx ↦ le_antisymm (hsup_y x hx sup_inf) (hsup_inf (sup_y x))
Cleared hypotheses: hsup_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
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 : β
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
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
⊢ inf_sup ≤ sup_inf
have a : Eq (α := Set β) {t : β | ∃ x ∈ X, sup_y x = t} {sup_inf}
Tactic: suffices {t | ∃ x ∈ X, sup_y x = t} = {sup_inf} from (this ▸ hinf_sup).unique (by simp) |>.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
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 : β
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
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
⊢ Eq (α := Set β) {t : β | ∃ x ∈ X, sup_y x = t} {sup_inf}
have a : ∀ (t : β), Membership.mem (γ := Set β) {t : β | ∃ x ∈ X, sup_y x = t} t ↔ Membership.mem (γ := Set β) {sup_inf} t
Tactic: ext t
-- 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
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 : β
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
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ (∃ x ∈ X, sup_y x = t) ↔ t = sup_inf
have a : (∃ x ∈ X, sup_y x = t) → t = sup_inf
Tactic: constructor
-- 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
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 : β
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
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
a : (∃ x ∈ X, sup_y x = t) → t = sup_inf
⊢ (∃ x ∈ X, sup_y x = t) ↔ t = sup_inf
have a₁ : t = sup_inf → ∃ x ∈ X, sup_y x = t
Tactic: constructor
-- 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
⊢ inf_sup ≤ sup_inf
have a : ∀ ⦃c : β⦄, c < inf_sup → c < sup_inf
Tactic: rw [← forall_lt_iff_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
ne_Y : Y.Nonempty
t : β
ht : t < inf_sup
⊢ ∃ (s : Finset (↑Y : Type u_2)), ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
have rw : X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t = ∅
Tactic: rw [← LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset kX hfy]
-- 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
⊢ X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t = ∅
have h : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t
Tactic: apply Set.eq_empty_of_forall_notMem
-- 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
x : E
hx : x ∈ X
hx' : Membership.mem (γ := Set E) (⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t) x
⊢ False
have hx'₁ : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
Tactic: simp only [mem_iInter, mem_preimage, mem_Iic] at hx'
Cleared hypotheses: 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
x : E
hx : x ∈ X
hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
⊢ False
have h : ∀ (ht : ∃ (c : β), Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ X, sup_y x_1 = x}) c ∧ t < c) (x : E)
  (hx : x ∈ X) (hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t), False
Tactic: rw [lt_isGLB_iff hinf_sup] at ht
Cleared hypotheses: ht, x, hx, 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 : ∃ (c : β), Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ X, sup_y x_1 = x}) c ∧ t < c
x : E
hx : x ∈ X
hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
⊢ False
have h : ∀ (c : β) (hc : Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ X, sup_y x_1 = x}) c) (htc : t < c), False
Tactic: obtain ⟨c, hc, htc⟩ := ht
Cleared hypotheses: ht
-- 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 : β
x : E
hx : x ∈ X
hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
c : β
hc : Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ X, sup_y x_1 = x}) c
htc : t < c
⊢ False
have hc₁ : ∀ a ∈ X, c ≤ sup_y a
Tactic: simp only [mem_lowerBounds, mem_setOf_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hc
Cleared hypotheses: hc
-- 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 : β
x : E
hx : x ∈ X
hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
c : β
htc : t < c
hc : ∀ a ∈ X, c ≤ sup_y a
⊢ False
have apply : sup_y x ≤ t
Tactic: apply not_le.mpr htc (le_trans (hc 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 : β
x : E
hx : x ∈ X
hx' : ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t
c : β
htc : t < c
hc : ∀ a ∈ X, c ≤ sup_y a
⊢ sup_y x ≤ t
have rw : ∀ (x_1 : β), Membership.mem (γ := Set β) {x_2 : β | ∃ y ∈ Y, f x y = x_2} x_1 → x_1 ≤ t
Tactic: rw [isLUB_le_iff (hsup_y x hx), mem_upperBounds]
-- 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
⊢ t < sup_inf
have this : ∃ (s : Finset (↑Y : Type u_2)), ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)
Tactic: have : ∃ s : Finset Y, ∀ x ∈ X, ∃ i ∈ s, t < f x i := by
    rw [← LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset kX hfy]
    apply Set.eq_empty_of_forall_notMem
    rintro x ⟨hx, hx'⟩
    simp only [mem_iInter, mem_preimage, mem_Iic] at hx'
    rw [lt_isGLB_iff hinf_sup] at ht
    obtain ⟨c, hc, htc⟩ := ht
    simp only [mem_lowerBounds, mem_setOf_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hc
    apply not_le.mpr htc (le_trans (hc x hx) _)
    rw [isLUB_le_iff (hsup_y x hx), mem_upperBounds]
    aesop