Theorem: ERealSion.minimax (Sion/Sion.lean)

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
apply symm
State after:
case a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y

State before:
case a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
apply le_antisymm
State after:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
exact iSup₂_iInf₂_le_iInf₂_iSup₂ X Y f
State after:
no goals

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
rw [← forall_lt_iff_le]
State after:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ∀ ⦃c : β⦄, c < ⨅ x ∈ X, ⨆ y ∈ Y, f x y → c < ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
⊢ ∀ ⦃c : β⦄, c < ⨅ x ∈ X, ⨆ y ∈ Y, f x y → c < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
intro t ht
State after:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
let X' (y : F) := ({x ∈ X | f x y ≤ t} : Set E)
State after:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
suffices hs : ∃ s : Set F, s ⊆ Y ∧ s.Finite ∧ (⋂ y ∈ s, X' y) = ∅ by
  obtain ⟨s, hsY, hs, hes⟩ := hs
  suffices hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y by
    obtain ⟨y0, hy0, ht0⟩ := exists_lt_iInf_of_lt_iInf_of_finite
      X ne_X cX kX Y cY f hfx hfx' hfy hfy' hs hst hsY
    simp only [lt_iSup_iff, exists_prop]
    use y0, hy0
    obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact
      ne_X kX (hfy y0 hy0)
    exact lt_of_lt_of_le (ht0 a ha) (le_iInf₂_iff.mpr h)
  intro x hx
  by_contra hx'
  push_neg at hx'
  rw [Set.eq_empty_iff_forall_not_mem] at hes
  apply hes x
  simp only [mem_iInter, mem_setOf_eq, X', forall₂_and]
  exact ⟨fun _ _ ↦ hx, hx'⟩
State after:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hs : ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
obtain ⟨s, hsY, hs, hes⟩ := hs
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
suffices hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y by
  obtain ⟨y0, hy0, ht0⟩ := exists_lt_iInf_of_lt_iInf_of_finite
    X ne_X cX kX Y cY f hfx hfx' hfy hfy' hs hst hsY
  simp only [lt_iSup_iff, exists_prop]
  use y0, hy0
  obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact
    ne_X kX (hfy y0 hy0)
  exact lt_of_lt_of_le (ht0 a ha) (le_iInf₂_iff.mpr h)
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
⊢ ∀ x ∈ X, ∃ y ∈ s, t < f x y

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
⊢ ∀ x ∈ X, ∃ y ∈ s, t < f x y
Tactic:
intro x hx
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
⊢ ∃ y ∈ s, t < f x y

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
⊢ ∃ y ∈ s, t < f x y
Tactic:
by_contra hx'
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
hx' : ¬∃ y ∈ s, t < f x y
⊢ False

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
hx' : ¬∃ y ∈ s, t < f x y
⊢ False
Tactic:
push_neg at hx'
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ False

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ False
Tactic:
rw [Set.eq_empty_iff_forall_not_mem] at hes
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ False

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ False
Tactic:
apply hes x
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ x ∈ ⋂ y ∈ s, X' y

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ x ∈ ⋂ y ∈ s, X' y
Tactic:
simp only [mem_iInter, mem_setOf_eq, X', forall₂_and]
State after:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ (∀ x_1 ∈ s, x ∈ X) ∧ ∀ x_1 ∈ s, f x x_1 ≤ t

State before:
case intro.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ∀ (x : E), x ∉ ⋂ y ∈ s, X' y
x : E
hx : x ∈ X
hx' : ∀ y ∈ s, f x y ≤ t
⊢ (∀ x_1 ∈ s, x ∈ X) ∧ ∀ x_1 ∈ s, f x x_1 ≤ t
Tactic:
exact ⟨fun _ _ ↦ hx, hx'⟩
State after:
no goals

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
obtain ⟨y0, hy0, ht0⟩ := exists_lt_iInf_of_lt_iInf_of_finite
  X ne_X cX kX Y cY f hfx hfx' hfy hfy' hs hst hsY
State after:
case intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y

State before:
case intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
simp only [lt_iSup_iff, exists_prop]
State after:
case intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ ∃ i ∈ Y, t < ⨅ x ∈ X, f x i

State before:
case intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ ∃ i ∈ Y, t < ⨅ x ∈ X, f x i
Tactic:
use y0, hy0
State after:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨅ x ∈ X, f x y0

State before:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨅ x ∈ X, f x y0
Tactic:
obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact
  ne_X kX (hfy y0 hy0)
State after:
case right.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
a : E
ha : a ∈ X
h : ∀ x ∈ X, f a y0 ≤ f x y0
⊢ t < ⨅ x ∈ X, f x y0

State before:
case right.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
a : E
ha : a ∈ X
h : ∀ x ∈ X, f a y0 ≤ f x y0
⊢ t < ⨅ x ∈ X, f x y0
Tactic:
exact lt_of_lt_of_le (ht0 a ha) (le_iInf₂_iff.mpr h)
State after:
no goals

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
let v : Y → Set E := fun y ↦ Exists.choose (hfyt y)
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
have hv : ∀ y, IsClosed (v y) ∧ X' y = X ∩ v y := fun y ↦ (hfyt y).choose_spec
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : ?m.390150
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
obtain ⟨s, hs⟩ := kX.elim_finite_subfamily_closed v (fun y => (hv y).1) hsZ
State after:
case intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅

State before:
case intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
have hs_ne : s.Nonempty := by
  rw [Finset.nonempty_iff_ne_empty]
  intro hs_e
  simp only [hs_e, Finset.not_mem_empty, iInter_of_empty, iInter_univ, inter_univ] at hs
  rw [Set.nonempty_iff_ne_empty] at ne_X
  exact ne_X hs
State after:
case intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅

State before:
case intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
use (Subtype.val : Y → F) '' (s : Set Y)
State after:
case h
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Subtype.val '' ↑s ⊆ Y ∧ Set.Finite (Subtype.val '' ↑s) ∧ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅

State before:
case h
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Subtype.val '' ↑s ⊆ Y ∧ Set.Finite (Subtype.val '' ↑s) ∧ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅
Tactic:
constructor
State after:
case h.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Subtype.val '' ↑s ⊆ Y

case h.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Set.Finite (Subtype.val '' ↑s) ∧ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ s.Nonempty
Tactic:
rw [Finset.nonempty_iff_ne_empty]
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ s ≠ ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ s ≠ ∅
Tactic:
intro hs_e
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_e : s = ∅
⊢ False

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_e : s = ∅
⊢ False
Tactic:
simp only [hs_e, Finset.not_mem_empty, iInter_of_empty, iInter_univ, inter_univ] at hs
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs_e : s = ∅
hs : X = ∅
⊢ False

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs_e : s = ∅
hs : X = ∅
⊢ False
Tactic:
rw [Set.nonempty_iff_ne_empty] at ne_X
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : X ≠ ∅
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs_e : s = ∅
hs : X = ∅
⊢ False

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : X ≠ ∅
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs_e : s = ∅
hs : X = ∅
⊢ False
Tactic:
exact ne_X hs
State after:
no goals

State before:
case h.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Subtype.val '' ↑s ⊆ Y
Tactic:
exact Subtype.coe_image_subset Y ↑s
State after:
no goals

State before:
case h.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Set.Finite (Subtype.val '' ↑s) ∧ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅
Tactic:
constructor
State after:
case h.right.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Set.Finite (Subtype.val '' ↑s)

case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅

State before:
case h.right.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Set.Finite (Subtype.val '' ↑s)
Tactic:
apply s.finite_toSet.image
State after:
no goals

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem] at hs ⊢
State after:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
⊢ ∀ (x : E), x ∉ ⋂ y ∈ Subtype.val '' ↑s, X' y

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
⊢ ∀ (x : E), x ∉ ⋂ y ∈ Subtype.val '' ↑s, X' y
Tactic:
intro x hx
State after:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : x ∈ ⋂ y ∈ Subtype.val '' ↑s, X' y
⊢ False

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : x ∈ ⋂ y ∈ Subtype.val '' ↑s, X' y
⊢ False
Tactic:
simp only [mem_image, Finset.mem_coe, SetCoe.exists, Subtype.coe_mk, exists_and_right,
  exists_eq_right, iInf_eq_iInter, iInter_exists, mem_iInter, mem_sep_iff] at hx
State after:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ False

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ False
Tactic:
apply hs x
State after:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X ∩ ⋂ i ∈ s, v i

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X ∩ ⋂ i ∈ s, v i
Tactic:
rw [iInter_coe_set, mem_inter_iff, mem_iInter]
State after:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X ∧ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }

State before:
case h.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X ∧ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }
Tactic:
constructor
State after:
case h.right.right.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X

case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }

State before:
case h.right.right.left
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ x ∈ X
Tactic:
obtain ⟨⟨j, hj⟩, hjs⟩ := hs_ne
State after:
case h.right.right.left.intro.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
j : F
hj : j ∈ Y
hjs : { val := j, property := hj } ∈ s
⊢ x ∈ X

State before:
case h.right.right.left.intro.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
j : F
hj : j ∈ Y
hjs : { val := j, property := hj } ∈ s
⊢ x ∈ X
Tactic:
exact (hx j hj hjs).1
State after:
no goals

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
⊢ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }
Tactic:
intro y
State after:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
⊢ x ∈ ⋂ (h : y ∈ Y), ⋂ (_ : { val := y, property := h } ∈ s), v { val := y, property := h }

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
⊢ x ∈ ⋂ (h : y ∈ Y), ⋂ (_ : { val := y, property := h } ∈ s), v { val := y, property := h }
Tactic:
rw [mem_iInter]
State after:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
⊢ ∀ (i : y ∈ Y), x ∈ ⋂ (_ : { val := y, property := i } ∈ s), v { val := y, property := i }

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
⊢ ∀ (i : y ∈ Y), x ∈ ⋂ (_ : { val := y, property := i } ∈ s), v { val := y, property := i }
Tactic:
intro hy
State after:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
⊢ x ∈ ⋂ (_ : { val := y, property := hy } ∈ s), v { val := y, property := hy }

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
⊢ x ∈ ⋂ (_ : { val := y, property := hy } ∈ s), v { val := y, property := hy }
Tactic:
rw [mem_iInter]
State after:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
⊢ { val := y, property := hy } ∈ s → x ∈ v { val := y, property := hy }

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
⊢ { val := y, property := hy } ∈ s → x ∈ v { val := y, property := hy }
Tactic:
intro hy'
State after:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ v { val := y, property := hy }

State before:
case h.right.right.right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ v { val := y, property := hy }
Tactic:
apply Set.inter_subset_right X
State after:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X ∩ v { val := y, property := hy }

State before:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X ∩ v { val := y, property := hy }
Tactic:
rw [← (hv (⟨y, hy⟩ : Y)).2]
State after:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X' ↑{ val := y, property := hy }

State before:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X' ↑{ val := y, property := hy }
Tactic:
simp only [Subtype.coe_mk, mem_sep_iff]
State after:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X' y

State before:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X' y
Tactic:
exact hx y hy hy'
State after:
no goals

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅
Tactic:
rw [← not_le] at ht
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ ∀ (x : E), x ∉ X ∩ ⋂ i, v i

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ ∀ (x : E), x ∉ X ∩ ⋂ i, v i
Tactic:
intro x hx
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ False

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ False
Tactic:
apply ht
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Tactic:
rw [mem_inter_iff, mem_iInter] at hx
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Tactic:
apply iInf₂_le_of_le x _ _
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ x ∈ X

β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ x ∈ X

β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Tactic:
exact hx.1
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Tactic:
simp only [iSup_le_iff]
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ∀ i ∈ Y, f x i ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ∀ i ∈ Y, f x i ≤ t
Tactic:
intro y hy
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ f x y ≤ t

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ f x y ≤ t
Tactic:
suffices x ∈ X' y by
  exact this.2
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ x ∈ X' y

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ x ∈ X' y
Tactic:
rw [(hv ⟨y, hy⟩).2]
State after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ x ∈ X ∩ v { val := y, property := hy }

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ x ∈ X ∩ v { val := y, property := hy }
Tactic:
exact ⟨hx.1, hx.2 ⟨y, hy⟩⟩
State after:
no goals

State before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
this : x ∈ X' y
⊢ f x y ≤ t
Tactic:
exact this.2
State after:
no goals

State before:
case a.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
⊢ ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
Tactic:
rintro ⟨y, hy⟩
State after:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy

State before:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy
Tactic:
specialize hfy y hy
State after:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : LowerSemicontinuousOn (fun x => f x y) X
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy

State before:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : LowerSemicontinuousOn (fun x => f x y) X
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy
Tactic:
simp_rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfy
State after:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy

State before:
case a.a.mk
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy
Tactic:
obtain ⟨v, v_closed, hv⟩ := hfy t
State after:
case a.a.mk.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy

State before:
case a.a.mk.intro.intro
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ ∃ vy, IsClosed vy ∧ X' ↑{ val := y, property := hy } = X ∩ vy
Tactic:
use v, v_closed
State after:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ X' ↑{ val := y, property := hy } = X ∩ v

State before:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ X' ↑{ val := y, property := hy } = X ∩ v
Tactic:
simp only [← hv]
State after:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ X' y = X ∩ (fun x => f x y) ⁻¹' Iic t

State before:
case right
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
y : F
hy : y ∈ Y
hfy : ∀ (b : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x y) ⁻¹' Iic b = X ∩ v
v : Set E
v_closed : IsClosed v
hv : X ∩ (fun x => f x y) ⁻¹' Iic t = X ∩ v
⊢ X' y = X ∩ (fun x => f x y) ⁻¹' Iic t
Tactic:
rfl
State after:
no goals