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)
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)
let S : Set (Set E) := { t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t }
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)

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
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)
rsuffices ⟨t, ⟨⟨x, hxt⟩, htclos, hst⟩, hBmin⟩ : ∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t
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
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
refine' zorn_superset _ fun F hFS hF => _
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

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
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
obtain rfl | hFnemp := F.eq_empty_or_nonempty
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)
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
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⟩
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)
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)
haveI : Nonempty (↥F) := hFnemp.to_subtype
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)
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)
rw [sInter_eq_iInter]
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
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)
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
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
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
obtain htu | hut := hF.total t.mem u.mem
no goals
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
exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
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}
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)
refine' ⟨x, mem_extremePoints_iff_extreme_singleton.2 _⟩
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
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}
rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]
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
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
by_contra hyx
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
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
obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
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
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
obtain ⟨z, hzt, hz⟩ :=
  (isCompact_of_isClosed_subset hscomp htclos hst.1).exists_forall_ge ⟨x, hxt⟩
    l.continuous.continuousOn
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
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
have h : IsExposed ℝ t ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) := fun _ => ⟨l, rfl⟩
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
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
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
no goals
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
exact hl.not_le (hyB.2 x hxt)
no goals
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
exact ⟨s, ⟨hsnemp, hscomp.isClosed, IsExtreme.rfl⟩, fun _ => False.elim⟩