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
t : β
hinfi_le : ∀ (y0 : F) (_ : y0 ∈ Y), ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x : F // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x (↑y1 : F)) (f x (↑y2 : F))
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ max (f x (↑y1 : F)) (f x (↑y2 : F))) X a
ht' : t' < max (f a (↑y1 : F)) (f a (↑y2 : F))
J1 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) := setOf_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J1 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y1 : F)
φ : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) ≃ₜ (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2) :=
  Homeomorph.setCongr (s := segment ℝ (↑y1 : F) (↑y2 : F)) (t := segment ℝ (↑y2 : F) (↑y1 : F)) ⋯
J2 : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2) :=
  preimage (β := (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (⇑φ : (a : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) → (↑(segment ℝ (↑y2 : F) (↑y1 : F)) : Type u_2))
    (setOf_sublevelLeft_subset X Y f t t' y2 y1)
mem_J2_iff :
  ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    z ∈ J2 ↔ sublevelLeft X f t (↑z : F) ⊆ sublevelLeft X f t' (↑y2 : F)
h_mem_Y : ∀ (z : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), (↑z : F) ∈ Y
hJ1J2 : ∀ (x : (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)), x ∉ J1 ∩ J2
hJ1_union_J2 :
  Subtype.val (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) '' (J1 ∪ J2) = segment ℝ (↑y1 : F) (↑y2 : F)
this :
  ∀ (u v : Set (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)),
    IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
hJ1 : IsClosed J1
hJ2 : IsClosed J2
h_univ : univ ⊆ J1 ∪ J2
h_inter : univ ∩ (J1 ∩ J2) = ∅
h2 : univ ⊆ J2
inr :
  sublevelLeft X f t
      (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) (↑y1 : F) ⋯ :
            { x : F // x ∈ segment ℝ (↑y1 : F) (↑y2 : F) }) :
        F) ⊆
    sublevelLeft X f t' (↑y1 : F)
inr₁ inr₂ : sublevelLeft X f t' (↑y1 : F) ⊆ sublevelLeft X f t' (↑y1 : F)
⊢ Membership.mem (α := (↑(segment ℝ (↑y1 : F) (↑y2 : F)) : Type u_2)) J1
    (Subtype.mk (p := fun (x : F) ↦ x ∈ segment ℝ (↑y1 : F) (↑y2 : F)) (↑y1 : F) ⋯ :
      { x : F // x ∈ segment ℝ (↑y1 : F) (↑y2 : F) })

Tactic:
grw [mem_J1_iff, monotone_sublevelLeft y1 htt'.le]

Premises used: LT.lt.le, _private.0.Sion.monotone_sublevelLeft
-- 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 : Set F
t : β
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 : ∅ ⊆ Y
ht : ∀ x ∈ X, ∃ (y : F), Membership.mem (γ := Set F) ∅ y ∧ t < f x y
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
simpa using ht _ ne_X.choose_spec

Premises used: Exists.choose_spec
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
⊢ b ∈ Y

Tactic:
have hb : (b ∈ Y) := hsY (mem_insert b s)
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
insert : ∀ (X'_e : X' = ∅), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
insert₁ : ∀ (X'_ne : X'.Nonempty), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
rcases Set.eq_empty_or_nonempty X' with X'_e | X'_ne

Premises used: Set.eq_empty_or_nonempty
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'_e : X' = ∅
right : ∀ x ∈ X, t < f x b
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
use b, hb
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'_e : X' = ∅
⊢ ∀ x ∈ X, t < f x b

Tactic:
simpa [X', Set.eq_empty_iff_forall_notMem] using X'_e

Premises used: Set.eq_empty_iff_forall_notMem
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
⊢ X' ⊆ X

Tactic:
have hX'X : X' ⊆ X := inter_subset_left
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
⊢ IsCompact X'

Tactic:
have kX' : IsCompact X' := (hfy b hb).isCompact_inter_preimage_Iic kX t
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'
⊢ Convex ℝ X'

Tactic:
have cX' : Convex ℝ X' := hfy' b hb t
-- 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
hrec :
  ∀ {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 : s ⊆ Y)
    (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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'
⊢ ∀ (hsY : s ⊆ Y) (ht : ∀ x ∈ X', ∃ y ∈ s, t < f x y), ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0

Tactic:
specialize hrec X'_ne kX'
      (fun y hy ↦ LowerSemicontinuousOn.mono (hfy y hy) hX'X)
      (fun y hy ↦ cX'.quasiconvexOn_restrict (hfy' y hy) hX'X)
      (fun x hx' ↦ hfx x (hX'X hx'))
      (fun x hx' ↦ hfx' x (hX'X hx'))
      cX'

Premises used: LowerSemicontinuousOn.mono, Convex.quasiconvexOn_restrict
-- 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 : E
hx : x ∈ X'
obtain : ∀ (y : F) (hy : y ∈ insert b s) (h : t < f x y), ∃ y ∈ s, t < f x y
⊢ ∃ y ∈ s, t < f x y

Tactic:
obtain ⟨y, hy, h⟩ := ht x hx.1

Premises used: And.left
-- 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_1 : 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 : E
hx : x ∈ X'
y : F
hy : y ∈ insert b s
h : t < f x y
inl :
  y ∉ s →
    ∀ (hsY : insert y s ⊆ Y) (ht : ∀ x ∈ X, ∃ y_1 ∈ insert y s, t < f x y_1) (hb : y ∈ Y),
      let X' := X ∩ (fun (x : E) ↦ f x y) ⁻¹' 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) (hx : x ∈ X'),
        ∃ y ∈ s, t < f x y
inr : ∀ (hy : y ∈ s), ∃ y ∈ s, t < f x y
⊢ ∃ y ∈ s, t < f x y

Tactic:
rcases hy with rfl | hy

Premises used: rfl
-- 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 : β
s : Set F
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
x : E
y : F
h : t < f x y
h_1 : y ∉ s
hsY : insert y s ⊆ Y
ht : ∀ x ∈ X, ∃ y_1 ∈ insert y s, t < f x y_1
hb : y ∈ Y
X' : Set E := X ∩ (fun (x : E) ↦ f x y) ⁻¹' 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
hx : x ∈ X'
⊢ ∃ y ∈ s, t < f x y

Tactic:
simp [h.not_ge hx.2]

Premises used: And.right, LT.lt.not_ge
-- 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_1 : 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 : E
hx : x ∈ X'
y : F
h : t < f x y
hy : y ∈ s
⊢ ∃ y ∈ s, t < f x y

Tactic:
⟨y, hy, h⟩

Premises used: And.intro, Exists.intro
-- 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_1 : 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 : E
hx : x ∈ X'
y : F
h : t < f x y
hy : y ∈ s
⊢ ∃ y ∈ s, t < f x y

Tactic:
exact ⟨y, hy, h⟩