[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
let S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
rsuffices ⟨t, ⟨⟨x, hxt⟩, htclos, hst⟩, hBmin⟩ : ∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
refine' ⟨x, mem_extremePoints_iff_extreme_singleton.2 _⟩
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ IsExtreme ℝ s {x}
[PROOFSTEP]
rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
⊢ y = x
[PROOFSTEP]
by_contra hyx
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
⊢ False
[PROOFSTEP]
obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
[GOAL]
case intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
⊢ False
[PROOFSTEP]
obtain ⟨z, hzt, hz⟩ :=
  (isCompact_of_isClosed_subset hscomp htclos hst.1).exists_forall_ge ⟨x, hxt⟩ l.continuous.continuousOn
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
⊢ False
[PROOFSTEP]
have h : IsExposed ℝ t ({z ∈ t | ∀ w ∈ t, l w ≤ l z}) := fun _ => ⟨l, rfl⟩
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
⊢ False
[PROOFSTEP]
rw [← hBmin ({z ∈ t | ∀ w ∈ t, l w ≤ l z}) ⟨⟨z, hzt, hz⟩, h.isClosed htclos, hst.trans h.isExtreme⟩ (t.sep_subset _)] at
  hyB 
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyx : ¬y = x
l : E →L[ℝ] ℝ
hyB : y ∈ {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
⊢ False
[PROOFSTEP]
exact hl.not_le (hyB.2 x hxt)
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ ∃ t, t ∈ S ∧ ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
[PROOFSTEP]
refine' zorn_superset _ fun F hFS hF => _
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ F → lb ⊆ s
[PROOFSTEP]
obtain rfl | hFnemp := F.eq_empty_or_nonempty
[GOAL]
case inl
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
hFS : ∅ ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ ∅ → lb ⊆ s
[PROOFSTEP]
exact ⟨s, ⟨hsnemp, hscomp.isClosed, IsExtreme.rfl⟩, fun _ => False.elim⟩
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ F → lb ⊆ s
[PROOFSTEP]
refine'
  ⟨⋂₀ F, ⟨_, isClosed_sInter fun t ht => (hFS ht).2.1, isExtreme_sInter hFnemp fun t ht => (hFS ht).2.2⟩, fun t ht =>
    sInter_subset_of_mem ht⟩
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
⊢ Set.Nonempty (⋂₀ F)
[PROOFSTEP]
haveI : Nonempty (↥F) := hFnemp.to_subtype
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
⊢ Set.Nonempty (⋂₀ F)
[PROOFSTEP]
rw [sInter_eq_iInter]
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
⊢ Set.Nonempty (⋂ (i : ↑F), ↑i)
[PROOFSTEP]
refine'
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ (fun t u => _) (fun t => (hFS t.mem).1)
    (fun t => isCompact_of_isClosed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t => (hFS t.mem).2.1
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
[PROOFSTEP]
obtain htu | hut := hF.total t.mem u.mem
[GOAL]
case inr.inl
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
htu : ↑t ⊆ ↑u
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
case inr.inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
hut : ↑u ⊆ ↑t
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
[PROOFSTEP]
exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure (↑(convexHull ℝ) (extremePoints ℝ s)) = s
[PROOFSTEP]
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
[PROOFSTEP]
by_contra hs
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
⊢ False
[PROOFSTEP]
obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
[GOAL]
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
⊢ False
[PROOFSTEP]
obtain ⟨l, r, hlr, hrx⟩ := geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
⊢ False
[PROOFSTEP]
have h : IsExposed ℝ s ({y ∈ s | ∀ z ∈ s, l z ≤ l y}) := fun _ => ⟨l, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
[PROOFSTEP]
obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
⊢ False
[PROOFSTEP]
obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
y : E
hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
[PROOFSTEP]
linarith [hlr _ (subset_closure <| subset_convexHull _ _ <| h.isExtreme.extremePoints_subset_extremePoints hy),
  hy.1.2 x hxA]
