awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.KreinMilman
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

Tactic:
⟨x, IsExtreme.mem_extremePoints ?_⟩

Premises used: IsExtreme.mem_extremePoints, Set.Nonempty, Exists.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
refine : IsExtreme ℝ s {x}
⊢ (extremePoints ℝ s).Nonempty

Tactic:
refine ⟨x, IsExtreme.mem_extremePoints ?_⟩
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
rwa : ∀ (y : E) (hyB : y ∈ t), y = x
⊢ IsExtreme ℝ s {x}

Tactic:
rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
by_contra : ∀ (hyx : ¬y = x), False
⊢ y = x

Tactic:
by_contra hyx
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
obtain : ∀ (l : StrongDual ℝ E) (hl : LT.lt (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) ((l : (a : E) → ℝ) x : ℝ)), False
⊢ False

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

Premises used: geometric_hahn_banach_point_point
-- Module: Mathlib.Analysis.Convex.KreinMilman
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 : ℝ)
obtain : ∀ (z : E) (hzt : z ∈ t) (hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) t z), False
⊢ False

Tactic:
obtain ⟨z, hzt, hz⟩ :=
      (hscomp.of_isClosed_subset htclos hst.1).exists_isMaxOn ⟨x, hxt⟩
        l.continuous.continuousOn

Premises used: IsExtreme.subset, Continuous.continuousOn, ContinuousLinearMap.continuous, IsCompact.of_isClosed_subset, Exists.intro, IsCompact.exists_isMaxOn
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.KreinMilman
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 : ℝ)}
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
⊢ 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

Premises used: IsExposed.isClosed, IsExposed.isExtreme, Minimal.eq_of_ge, IsExtreme.trans, And.intro, Exists.intro, Set.sep_subset
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
hyx : ¬y = x
l : StrongDual ℝ E
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:
hl.not_ge (hyB.2 x hxt)

Premises used: And.right, LT.lt.not_ge
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
hyx : ¬y = x
l : StrongDual ℝ E
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:
exact hl.not_ge (hyB.2 x hxt)

Premises used: And.right, LT.lt.not_ge
-- Module: Mathlib.Analysis.Convex.KreinMilman
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

Tactic:
zorn_superset _ fun F hFS hF => ?_

Premises used: zorn_superset
-- Module: Mathlib.Analysis.Convex.KreinMilman
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}
refine : ∀ (F : Set (Set E)) (hFS : F ⊆ S) (hF : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) F), ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
⊢ ∃ (t : Set E), Minimal (fun (x : Set E) ↦ x ∈ S) t

Tactic:
refine zorn_superset _ fun F hFS hF => ?_

Premises used: zorn_superset
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
inr : ∀ (hFnemp : F.Nonempty), ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
⊢ ∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s

Tactic:
obtain rfl | hFnemp := F.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.KreinMilman
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}
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:
⟨s, ⟨hsnemp, hscomp.isClosed, IsExtreme.rfl⟩, fun _ => False.elim⟩

Premises used: False.elim, IsExtreme.rfl, And.intro, Exists.intro, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.KreinMilman
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}
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:
exact ⟨s, ⟨hsnemp, hscomp.isClosed, IsExtreme.rfl⟩, fun _ => False.elim⟩
-- Module: Mathlib.Analysis.Convex.KreinMilman
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

Tactic:
⟨⋂₀ 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⟩

Premises used: Set.sInter_subset_of_mem, And.right, And.left, isExtreme_sInter, And.intro, isClosed_sInter, Exists.intro, Set.sInter
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
inr : (⋂₀ 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⟩
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
⊢ Nonempty.{u_1 + 1} (↑F : Type u_1)

Tactic:
haveI : Nonempty (↥F) := hFnemp.to_subtype
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
inr : Set.Nonempty.{u_1} (α := E) (⋂ (i : (↑F : Type u_1)), (↑i : Set E))
⊢ (⋂₀ F).Nonempty

Tactic:
rw [sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.Analysis.Convex.KreinMilman
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))

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

Premises used: IsExtreme.subset, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, IsCompact.of_isClosed_subset, And.right, And.left, Subtype.mem
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
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)
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (i : (↑F : Type u_1)), (↑i : 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

Premises used: IsExtreme.subset, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, IsCompact.of_isClosed_subset, And.right, And.left
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
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)
⊢ ∃ (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

Premises used: Subtype.mem, IsChain.total
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
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:
⟨t, Subset.rfl, htu⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
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:
⟨u, hut, Subset.rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
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)
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:
exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
apply : s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
⊢ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s)) = s

Tactic:
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm

Premises used: closure_minimal, HasSubset.Subset.antisymm, convexHull_min, extremePoints_subset, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
by_contra : ∀ (hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))), False
⊢ s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))

Tactic:
by_contra hs
-- Module: Mathlib.Analysis.Convex.KreinMilman
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))
obtain : ∀ (x : E) (hxA : x ∈ s) (hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))), False
⊢ False

Tactic:
obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.Analysis.Convex.KreinMilman
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))
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
⊢ False

Tactic:
obtain ⟨l, r, hlr, hrx⟩ :=
    geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt

Premises used: Convex.closure, convex_convexHull, geometric_hahn_banach_closed_point, isClosed_closure
-- Module: Mathlib.Analysis.Convex.KreinMilman
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
⊢ 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⟩