awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ),
    (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, -1, by simp, fun b _hb => by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
inr :
  ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₃ : IsOpen.{u_2} (X := E) ∅) (disj : Disjoint s ∅),
    ∃ (f : StrongDual ℝ E) (u : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → u < (f : (a : E) → ℝ) b
inr₁ :
  ∀ (b₀ : E) (hb₀ : b₀ ∈ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex.{0, u_2} ℝ (E := E) ∅
ht₃ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint s ∅
a : E
_ha : a ∈ s
⊢ LT.lt (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex.{0, u_2} ℝ (E := E) ∅
ht₃ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint s ∅
⊢ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → LT.lt (α := ℝ) (1 : ℝ) ((0 : (a : E) → ℝ) b : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex.{0, u_2} ℝ (E := E) ∅
ht₃ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint s ∅
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ),
    (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → u < (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, 1, fun a _ha => by simp, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
inr :
  ∀ (f : StrongDual ℝ E) (s_1 : ℝ) (hf₁ : ∀ a ∈ s, (f : (a : E) → ℝ) a < s_1)
    (hf₂ : ∀ b ∈ t, s_1 ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
obtain ⟨f, s, hf₁, hf₂⟩ := geometric_hahn_banach_open hs₁ hs₂ ht₁ disj

Premises used: geometric_hahn_banach_open
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s_1, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
⟨f, s, hf₁, image_subset_iff.1 (?_ : f '' t ⊆ Ioi s)⟩

Premises used: And.intro, Exists.intro, Iff.mp, Set.image_subset_iff
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
inr : (⇑f : (a : E) → ℝ) '' t ⊆ Ioi s
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s_1, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
refine ⟨f, s, hf₁, image_subset_iff.1 (?_ : f '' t ⊆ Ioi s)⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
inr : (⇑f : (a : E) → ℝ) '' t ⊆ interior (Ici s)
⊢ (⇑f : (a : E) → ℝ) '' t ⊆ Ioi s

Tactic:
rw [← interior_Ici]

Premises used: interior_Ici
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
⊢ (⇑f : (a : E) → ℝ) '' t ⊆ interior (Ici s)

Tactic:
interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero ?_ _ ht₃)

Premises used: Iff.mpr, interior_maximal, Set.image_subset_iff, ContinuousLinearMap.isOpenMap_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
inr : f ≠ 0
⊢ (⇑f : (a : E) → ℝ) '' t ⊆ interior (Ici s)

Tactic:
refine interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero ?_ _ ht₃)

Premises used: Iff.mpr, interior_maximal, Set.image_subset_iff, ContinuousLinearMap.isOpenMap_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ a ∈ s_1, 0 < s
hf₂ : ∀ b ∈ t, s ≤ 0
⊢ False

Tactic:
(hf₁ _ ha₀).not_ge (hf₂ _ hb₀)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ a ∈ s_1, 0 < s
hf₂ : ∀ b ∈ t, s ≤ 0
⊢ False

Tactic:
exact (hf₁ _ ha₀).not_ge (hf₂ _ hb₀)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
obtain :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u)
    (hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
obtain ⟨f, u, hfA, hfB⟩ :=
    geometric_hahn_banach_open hs.interior isOpen_interior ht hst

Premises used: geometric_hahn_banach_open, isOpen_interior, Convex.interior
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
⟨f, u, ?_, fun a ha ↦ ?_, hfB⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
refine_1 : f ≠ 0
refine_2 : ∀ (a : E) (ha : a ∈ s), (f : (a : E) → ℝ) a ≤ u
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
refine ⟨f, u, ?_, fun a ha ↦ ?_, hfB⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
refine_1 : ∀ (a : E) (ha : a ∈ interior s), f ≠ 0
⊢ f ≠ 0

Tactic:
obtain ⟨a, ha⟩ := hsint
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
refine_1 : ∀ (b : E) (hb : b ∈ t), f ≠ 0
⊢ f ≠ 0

Tactic:
obtain ⟨b, hb⟩ := htne
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
⊢ 0 < u

Tactic:
simpa [hzero] using hfA a ha
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
⊢ 0 < u

Tactic:
have ha' : (0 : ℝ) < u := by simpa [hzero] using hfA a ha
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
ha' : 0 < u
⊢ u ≤ 0

Tactic:
simpa [hzero] using hfB b hb
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
ha' : 0 < u
⊢ u ≤ 0

Tactic:
have hb' : u ≤ (0 : ℝ) := by simpa [hzero] using hfB b hb
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
ha' : 0 < u
hb' : u ≤ 0
linarith : 0 - u + (u - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ s
refine_2 : a ∈ closure (interior s)
⊢ (f : (a : E) → ℝ) a ≤ u

Tactic:
apply closure_minimal (fun x hx => le_of_lt (hfA x hx)) <| isClosed_Iic.preimage f.continuous

Premises used: closure_minimal, le_of_lt, isClosed_Iic, ContinuousLinearMap.continuous, IsClosed.preimage
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ s
⊢ a ∈ closure (interior s)

Tactic:
simpa [hs.closure_interior_eq_closure_of_nonempty_interior hsint] using subset_closure ha

Premises used: subset_closure, Convex.closure_interior_eq_closure_of_nonempty_interior
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
pos :
  ∀ (htne : t.Nonempty),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
neg :
  ∀ (htne : ¬t.Nonempty),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
by_cases htne : t.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
pos :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (hs' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) (ht' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
obtain ⟨f, u, -, hs', ht'⟩ :=
      geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne

Premises used: geometric_hahn_banach_of_nonempty_interior
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hs' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
ht' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
⟨f, u, hs', ht'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hs' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
ht' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
exact ⟨f, u, hs', ht'⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ (∀ a ∈ s, LE.le (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (0 : ℝ)) ∧
    ∀ b ∈ t, LE.le (α := ℝ) (0 : ℝ) ((0 : (a : E) → ℝ) b : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, 0, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
obtain :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (hfne : f ≠ 0) (hA' : ∀ a ∈ A, (f : (a : E) → ℝ) a ≤ u)
    (hx' : ∀ (b : E), Membership.mem (γ := Set E) {x} b → u ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
obtain ⟨f, u, hfne, hA', hx'⟩ :=
    geometric_hahn_banach_of_nonempty_interior hA (convex_singleton x)
      (disjoint_singleton_right.2 hxA) hAint (singleton_nonempty x)

Premises used: Iff.mpr, Set.singleton_nonempty, Set.disjoint_singleton_right, convex_singleton, geometric_hahn_banach_of_nonempty_interior
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ A, (f : (a : E) → ℝ) a ≤ u
hx' : ∀ (b : E), Membership.mem (γ := Set E) {x} b → u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
⟨f, hfne, fun a ha => (hA' a ha).trans (hx' x (mem_singleton _))⟩

Premises used: Set.mem_singleton, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ A, (f : (a : E) → ℝ) a ≤ u
hx' : ∀ (b : E), Membership.mem (γ := Set E) {x} b → u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
exact ⟨f, hfne, fun a ha => (hA' a ha).trans (hx' x (mem_singleton _))⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
inl :
  ∀ (hs₁ : Convex.{0, u_2} ℝ (E := E) ∅) (hs₂ : IsCompact.{u_2} (X := E) ∅) (disj : Disjoint ∅ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
inr :
  ∀ (hs : s.Nonempty),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsCompact.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ (∀ (a : E), Membership.mem (γ := Set E) ∅ a → LT.lt (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (-2 : ℝ)) ∧
    LT.lt (α := ℝ) (-2) (-1) ∧ ∀ b ∈ t, LT.lt (α := ℝ) (-1 : ℝ) ((0 : (a : E) → ℝ) b : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsCompact.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
    (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, -2, -1, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
inr :
  ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₂ : IsClosed.{u_2} (X := E) ∅) (disj : Disjoint s ∅),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → v < (f : (a : E) → ℝ) b
inr₁ :
  ∀ (_ht : t.Nonempty),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b

Tactic:
obtain rfl | _ht := t.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl