-- Mathlib/Analysis/Convex/KreinMilman.lean
theorem IsCompact.extremePoints_nonempty (hscomp : IsCompact s) (hsnemp : s.Nonempty) :
    (s.extremePoints ℝ).Nonempty

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
⊢ y = x

Tactic:
by_contra hyx

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
⊢ False

Proof state:
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 => x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s

Tactic:
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⟩

Result:
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 => x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ (⋂₀ F).Nonempty

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
⊢ False

Tactic:
obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx

Result:
case intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) 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

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 => x1 ⊆ x2) F
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s

Tactic:
obtain rfl | hFnemp := F.eq_empty_or_nonempty

Result:
case inl
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
hFS : ∅ ⊆ S
hF : IsChain (fun x1 x2 => x1 ⊆ x2) ∅
⊢ ∃ lb ∈ S, ∀ s ∈ ∅, lb ⊆ s

case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 => x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s

Proof state:
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) 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 : IsMaxOn (⇑l) t z
⊢ False

Tactic:
have h : IsExposed ℝ t ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) := fun _ => ⟨l, rfl⟩

Result:
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x => x ∈ S) 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 : IsMaxOn (⇑l) t z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
⊢ False