awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
rsuffices : ∀ (t : Set E) (ht : Minimal (fun (x : Set E) ↦ x ∈ S) t), (extremePoints ℝ s).Nonempty
⊢ (extremePoints ℝ s).Nonempty
have rsuffices₁ : ∃ (t : Set E), Minimal (fun (x : Set E) ↦ x ∈ S) t
Tactic: rsuffices ⟨t, ht⟩ : ∃ t, Minimal (· ∈ S) t
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
⊢ (extremePoints ℝ s).Nonempty
have obtain : ∀ (x : E) (hxt : x ∈ t) (htclos : IsClosed t) (hst : IsExtreme ℝ s t), (extremePoints ℝ s).Nonempty
Tactic: obtain ⟨⟨x, hxt⟩, htclos, hst⟩ := ht.prop
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ (extremePoints ℝ s).Nonempty
have refine : IsExtreme ℝ s {x}
Tactic: refine ⟨x, IsExtreme.mem_extremePoints ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ IsExtreme ℝ s {x}
have rwa : ∀ (y : E) (hyB : y ∈ t), y = x
Tactic: rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
⊢ y = x
have by_contra : ∀ (hyx : ¬y = x), False
Tactic: by_contra hyx
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
⊢ False
have obtain : ∀ (l : StrongDual ℝ E) (hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)), False
Tactic: obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : StrongDual ℝ E
hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)
⊢ False
have obtain : ∀ (z : E) (hzt : z ∈ t) (hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) t z), False
Tactic: obtain ⟨z, hzt, hz⟩ :=
      (hscomp.of_isClosed_subset htclos hst.1).exists_isMaxOn ⟨x, hxt⟩
        l.continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : StrongDual ℝ E
hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)
z : E
hzt : z ∈ t
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) t z
⊢ False
have h : IsExposed ℝ t {z : E | z ∈ t ∧ ∀ w ∈ t, LE.le (α := ℝ) ((l : (a : E) → ℝ) w : ℝ) ((l : (a : E) → ℝ) z : ℝ)}
Tactic: have h : IsExposed ℝ t ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) := fun _ => ⟨l, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : StrongDual ℝ E
hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)
z : E
hzt : z ∈ t
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) t z
h : IsExposed ℝ t {z : E | z ∈ t ∧ ∀ w ∈ t, LE.le (α := ℝ) ((l : (a : E) → ℝ) w : ℝ) ((l : (a : E) → ℝ) z : ℝ)}
⊢ False
have rw : ∀
  (hyB :
    Membership.mem (γ := Set E)
      {z : E | z ∈ t ∧ ∀ w ∈ t, LE.le (α := ℝ) ((l : (a : E) → ℝ) w : ℝ) ((l : (a : E) → ℝ) z : ℝ)} y)
  (hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)) (z : E) (hzt : z ∈ t)
  (hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) t z)
  (h : IsExposed ℝ t {z : E | z ∈ t ∧ ∀ w ∈ t, LE.le (α := ℝ) ((l : (a : E) → ℝ) w : ℝ) ((l : (a : E) → ℝ) z : ℝ)}),
  False
Tactic: rw [ht.eq_of_ge (y := ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }))
      ⟨⟨z, hzt, hz⟩, h.isClosed htclos, hst.trans h.isExtreme⟩ (t.sep_subset _)] at hyB
Cleared hypotheses: hyB, hl, z, hzt, hz, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ ∃ (t : Set E), Minimal (fun (x : Set E) ↦ x ∈ S) t
have refine : ∀ (F : Set (Set E)) (hFS : F ⊆ S) (hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F), ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
Tactic: refine zorn_superset _ fun F hFS hF => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
have inl : ∀ (hFS : ∅ ⊆ S) (hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) ∅),
  ∃ lb ∈ S, ∀ (s : Set E), Membership.mem (γ := Set (Set E)) ∅ s → lb ⊆ s
Tactic: obtain rfl | hFnemp := F.eq_empty_or_nonempty
Cleared hypotheses: F, hFS, hF
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
inl :
  ∀ (hFS : ∅ ⊆ S) (hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) ∅),
    ∃ lb ∈ S, ∀ (s : Set E), Membership.mem (γ := Set (Set E)) ∅ s → lb ⊆ s
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
have inr : ∀ (hFnemp : F.Nonempty), ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
Tactic: obtain rfl | hFnemp := F.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
have inr : (⋂₀ F).Nonempty
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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ (⋂₀ F).Nonempty
have this : Nonempty.{u_1 + 1} (↑F : Type u_1)
Tactic: haveI : Nonempty (↥F) := hFnemp.to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty.{u_1 + 1} (↑F : Type u_1)
⊢ (⋂₀ F).Nonempty
have inr : Set.Nonempty.{u_1} (α := E) (⋂ (i : (↑F : Type u_1)), (↑i : Set E))
Tactic: rw [sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty.{u_1 + 1} (↑F : Type u_1)
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (i : (↑F : Type u_1)), (↑i : Set E))
have inr : ∀ (t u : (↑F : Type u_1)),
  ∃ (z : (↑F : Type u_1)),
    (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
Tactic: refine IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun t u => ?_)
    (fun t => (hFS t.mem).1)
    (fun t => hscomp.of_isClosed_subset (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t =>
      (hFS t.mem).2.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty.{u_1 + 1} (↑F : Type u_1)
t u : (↑F : Type u_1)
⊢ ∃ (z : (↑F : Type u_1)),
    (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
have inr : ∀ (htu : (↑t : Set E) ⊆ (↑u : Set E)),
  ∃ (z : (↑F : Type u_1)),
    (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
Tactic: obtain htu | hut := hF.total t.mem u.mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty.{u_1 + 1} (↑F : Type u_1)
t u : (↑F : Type u_1)
inr :
  ∀ (htu : (↑t : Set E) ⊆ (↑u : Set E)),
    ∃ (z : (↑F : Type u_1)),
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
        (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
⊢ ∃ (z : (↑F : Type u_1)),
    (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
have inr₁ : ∀ (hut : (↑u : Set E) ⊆ (↑t : Set E)),
  ∃ (z : (↑F : Type u_1)),
    (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑t : Set E) (↑z : Set E) ∧
      (fun (x1 x2 : Set E) ↦ x1 ⊇ x2) (↑u : Set E) (↑z : Set E)
Tactic: obtain htu | hut := hF.total t.mem u.mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s)) = s
have apply : s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
Tactic: apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
have by_contra : ∀ (hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))), False
Tactic: by_contra hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
⊢ False
have obtain : ∀ (x : E) (hxA : x ∈ s) (hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))), False
Tactic: obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
⊢ False
have obtain : ∀ (l : StrongDual ℝ E) (r : ℝ)
  (hlr :
    ∀ (a : E),
      Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
        (l : (a : E) → ℝ) a < r)
  (hrx : r < (l : (a : E) → ℝ) x), False
Tactic: obtain ⟨l, r, hlr, hrx⟩ :=
    geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
⊢ False
have h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
Tactic: have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
⊢ False
have obtain : ∀ (z : E) (hzA : z ∈ s) (hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z), False
Tactic: obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
z : E
hzA : z ∈ s
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z
⊢ False
have obtain : ∀ (y : E)
  (hy :
    Membership.mem (γ := Set E)
      (extremePoints ℝ {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)})
      y),
  False
Tactic: obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
z : E
hzA : z ∈ s
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z
y : E
hy :
  Membership.mem (γ := Set E)
    (extremePoints ℝ {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}) y
⊢ False
have linarith : HSub.hSub (β := ℝ) r ((l : (a : E) → ℝ) x : ℝ) + HSub.hSub (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) r +
    HSub.hSub (α := ℝ) (β := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ) =
  0
Tactic: linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
    h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) w
have ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
Tactic: have ht : IsCompact {x ∈ s | f x = w} :=
    hs.inter_right <| isClosed_singleton.preimage f.continuous
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) w
have ht₀ : Set.Nonempty.{u_1} (α := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
Tactic: have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw