awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
a : ∀ ⦃c : β⦄, c < inf_sup → c < sup_inf
⊢ inf_sup ≤ sup_inf

Tactic:
rw [← forall_lt_iff_le]

Premises used: forall_lt_iff_le
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
rw : X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t = ∅
⊢ ∃ (s : Finset (↑Y : Type u_2)), ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)

Tactic:
rw [← LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset kX hfy]

Premises used: LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
h : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t
⊢ X ∩ ⋂ i ∈ Y, (fun (x : E) ↦ f x i) ⁻¹' Iic t = ∅

Tactic:
apply Set.eq_empty_of_forall_notMem

Premises used: Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
⊢ ∀ (i : F) (i_1 : i ∈ Y), f x i ≤ t

Tactic:
simp only [mem_iInter, mem_preimage, mem_Iic] at hx'

Premises used: Set.mem_iInter, Set.mem_Iic, Set.mem_preimage
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
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
⊢ False

Tactic:
rw [lt_isGLB_iff hinf_sup] at ht

Premises used: lt_isGLB_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
h : ∀ (c : β) (hc : Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ X, sup_y x_1 = x}) c) (htc : t < c), False
⊢ False

Tactic:
obtain ⟨c, hc, htc⟩ := ht
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
⊢ ∀ 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

Premises used: and_imp, forall_exists_index, mem_lowerBounds, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
apply : sup_y x ≤ t
⊢ False

Tactic:
apply not_le.mpr htc (le_trans (hc x hx) _)

Premises used: not_le, Iff.mpr, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
rw : ∀ (x_1 : β), Membership.mem (γ := Set β) {x_2 : β | ∃ y ∈ Y, f x y = x_2} x_1 → x_1 ≤ t
⊢ sup_y x ≤ t

Tactic:
rw [isLUB_le_iff (hsup_y x hx), mem_upperBounds]

Premises used: isLUB_le_iff, mem_upperBounds
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
⊢ ∀ (x_1 : β), Membership.mem (γ := Set β) {x_2 : β | ∃ y ∈ Y, f x y = x_2} x_1 → x_1 ≤ t

Tactic:
aesop
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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)

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
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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)
a : ∀ (s : Finset (↑Y : Type u_2)) (hs : ∀ x ∈ X, ∃ i ∈ s, t < f x (↑i : F)), t < sup_inf
⊢ t < sup_inf

Tactic:
obtain ⟨s, hs⟩ := this
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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
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
⊢ ∃ 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
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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)
h : (↑i : F) ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)) ∧ 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:
use i.val

Premises used: Subtype.val
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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)
⊢ (↑i : F) ∈ Subtype.val (p := fun (x : F) ↦ x ∈ Y) '' (↑s : Set (↑Y : Type u_2)) ∧ t < f x (↑i : F)

Tactic:
simp [hi, hi']
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
cY : Convex ℝ Y
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

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']