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 β
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
⊢ ∀ x ∈ X', ∃ y ∈ s, t < f x y

Tactic:
have ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y := by
        /- otherwise, if  infi x ∈ X', supr y ∈ s f x y ≤ t
          then for every t' > t, there is x ∈ X' such that supr y ∈ s f x y ≤ t',
          since x ∈ X' and t ≤ t', we have supr y ∈ insert b s f x y  ≤ t',
          hence infi x ∈ X, supr y ∈ insert b s, f x y ≤ t',
          so that infi x ∈ X, supr y ∈ insert b s, f x y ≤ t. -/
      intro x hx
      obtain ⟨y, hy, h⟩ := ht x hx.1
      rcases hy with rfl | hy
      · simp [h.not_ge hx.2]
      · exact ⟨y, hy, h⟩
-- Module: Mathlib.Topology.Sion
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
grw₁ grw₂ : Y ⊆ Y
⊢ s ⊆ Y

Tactic:
grw [subset_insert b s, hsY]

Premises used: Set.subset_insert
-- Module: Mathlib.Topology.Sion
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.insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ Insert.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
insert : ∀ (y1 : F) (hy1 : y1 ∈ Y) (hty1 : ∀ x ∈ X', t < f x y1), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
obtain ⟨y1, hy1, hty1⟩ := hrec (by grw [subset_insert b s, hsY]) ht_lt
-- Module: Mathlib.Topology.Sion
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

Tactic:
exists_lt_iInf_of_lt_iInf_of_sup ne_X kX hfy hfy' cY hfx hfx' hb hy1 fun x hx ↦ ?_

Premises used: Sion.exists_lt_iInf_of_lt_iInf_of_sup
-- Module: Mathlib.Topology.Sion
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.insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ Insert.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
insert : ∀ (x : E) (hx : x ∈ X), t < max (f x b) (f x y1)
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
refine exists_lt_iInf_of_lt_iInf_of_sup ne_X kX hfy hfy' cY hfx hfx' hb hy1 fun x hx ↦ ?_

Premises used: Sion.exists_lt_iInf_of_lt_iInf_of_sup
-- Module: Mathlib.Topology.Sion
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)
neg : ∀ (hx' : x ∉ X'), t < max (f x b) (f x y1)
⊢ t < max (f x b) (f x y1)

Tactic:
by_cases hx' : x ∈ X'
-- Module: Mathlib.Topology.Sion
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)

Tactic:
(hty1 x hx').trans_le (le_sup_right)

Premises used: le_sup_right, LT.lt.trans_le
-- Module: Mathlib.Topology.Sion
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)

Tactic:
exact (hty1 x hx').trans_le (le_sup_right)

Premises used: le_sup_right, LT.lt.trans_le
-- Module: Mathlib.Topology.Sion
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'
apply : t < f x b
⊢ t < max (f x b) (f x y1)

Tactic:
apply lt_of_lt_of_le _ (le_sup_left)

Premises used: le_sup_left, lt_of_lt_of_le
-- Module: Mathlib.Topology.Sion
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'
rw : ¬f x b ≤ t
⊢ t < f x b

Tactic:
rw [← not_le]

Premises used: not_le
-- Module: Mathlib.Topology.Sion
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'
⊢ ¬f x b ≤ t

Tactic:
fun h ↦ hx' ⟨hx, h⟩

Premises used: And.intro, Not
-- Module: Mathlib.Topology.Sion
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'
⊢ ¬f x b ≤ t

Tactic:
exact fun h ↦ hx' ⟨hx, h⟩

Premises used: And.intro
-- 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
a : sup_inf = inf_sup
⊢ inf_sup = sup_inf

Tactic:
apply symm

Premises used: symm
-- 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
a : sup_inf ≤ inf_sup
a₁ : inf_sup ≤ sup_inf
⊢ sup_inf = inf_sup

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
a : ∀ (x : β), Membership.mem (γ := Set β) {x : β | ∃ x_1 ∈ X, sup_y x_1 = x} x → sup_inf ≤ x
⊢ sup_inf ≤ inf_sup

Tactic:
rw [le_isGLB_iff hinf_sup, mem_lowerBounds]

Premises used: mem_lowerBounds, le_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
x : E
hx : x ∈ X
a : ∀ (x_1 : β), Membership.mem (γ := Set β) {x : β | ∃ y ∈ Y, inf_x y = x} x_1 → x_1 ≤ sup_y x
⊢ sup_inf ≤ sup_y x

Tactic:
rw [isLUB_le_iff hsup_inf, 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
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
trans : inf_x y ≤ f x y
trans₁ : f x y ≤ sup_y x
⊢ inf_x y ≤ sup_y x

Tactic:
trans f x y