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
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : s.Nonempty
ht₁ : Convex.{0, u_2} ℝ (E := E) ∅
ht₂ : IsClosed.{u_2} (X := E) ∅
disj : Disjoint s ∅
⊢ (∀ a ∈ s, LT.lt (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (1 : ℝ)) ∧
    LT.lt (α := ℝ) 1 2 ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → LT.lt (α := ℝ) (2 : ℝ) ((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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : s.Nonempty
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

Tactic:
exact ⟨0, 1, 2, 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
_ht : t.Nonempty
inr :
  ∀ (U V : Set E) (hU : IsOpen U) (hV : IsOpen V) (hU₁ : Convex ℝ U) (hV₁ : Convex ℝ V) (sU : s ⊆ U) (tV : t ⊆ V)
    (disj' : Disjoint U V),
    ∃ (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 ⟨U, V, hU, hV, hU₁, hV₁, sU, tV, disj'⟩ := disj.exists_open_convexes hs₁ hs₂ ht₁ ht₂

Premises used: Disjoint.exists_open_convexes
-- 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
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
inr :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u) (hf₂ : ∀ b ∈ V, u < (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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b

Tactic:
obtain ⟨f, u, hf₁, hf₂⟩ := geometric_hahn_banach_open_open hU₁ hU hV₁ hV disj'

Premises used: geometric_hahn_banach_open_open
-- 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
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
inr :
  ∀ (x : E) (hx₁ : x ∈ s) (hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x),
    ∃ (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 ⟨x, hx₁, hx₂⟩ := hs₂.exists_isMaxOn hs f.continuous.continuousOn

Premises used: Continuous.continuousOn, ContinuousLinearMap.continuous, IsCompact.exists_isMaxOn
-- 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
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
⊢ (f : (a : E) → ℝ) x < u

Tactic:
have : f x < u := hf₁ x (sU hx₁)
-- 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
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this : (f : (a : E) → ℝ) x < u
a : E
ha : a ∈ s
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ LE.le (α := ℝ) ((f : (a : E) → ℝ) x_2 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) x_1} a

Tactic:
have := hx₂ 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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this_1 : (f : (a : E) → ℝ) x < u
a : E
ha : a ∈ s
this : LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
linarith : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → 2 / 2 = 1
linarith₁ : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → GT.gt (α := ℝ) 2 0
linarith₃ :
  HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a →
    HSub.hSub (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u +
          2 * HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ) +
        (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : E) → ℝ) x : ℝ) + 1 * u -
          HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((f : (a : E) → ℝ) a : ℝ)) =
      0
linarith₄ : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → GT.gt (α := ℝ) 2 0
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2

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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this : (f : (a : E) → ℝ) x < u
linarith : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → 2 / 2 = 1
linarith₁ : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → GT.gt (α := ℝ) 2 0
linarith₃ :
  u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 →
    HSub.hSub (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u +
        (2 * u - (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : E) → ℝ) x : ℝ) + 1 * u)) =
      0
⊢ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 < u

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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this : (f : (a : E) → ℝ) x < u
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b

Tactic:
exact
    ⟨f, (f x + u) / 2, u,
      fun a ha => by have := hx₂ ha; dsimp at this; linarith,
      by linarith,
      fun b hb => hf₂ b (tV hb)⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
ht₁ : Convex ℝ t_1
ht₂ : IsCompact t_1
disj : Disjoint s_1 t_1
f : StrongDual ℝ E
s t : ℝ
hs : ∀ a ∈ t_1, (f : (a : E) → ℝ) a < s
st : s < t
ht : ∀ b ∈ s_1, t < (f : (a : E) → ℝ) b
⊢ ∀ a ∈ s_1, (-f : (a : E) → ℝ) a < -t

Tactic:
simpa using ht
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
ht₁ : Convex ℝ t_1
ht₂ : IsCompact t_1
disj : Disjoint s_1 t_1
f : StrongDual ℝ E
s t : ℝ
hs : ∀ a ∈ t_1, (f : (a : E) → ℝ) a < s
st : s < t
ht : ∀ b ∈ s_1, t < (f : (a : E) → ℝ) b
⊢ -t < -s

Tactic:
simpa using st
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
ht₁ : Convex ℝ t_1
ht₂ : IsCompact t_1
disj : Disjoint s_1 t_1
f : StrongDual ℝ E
s t : ℝ
hs : ∀ a ∈ t_1, (f : (a : E) → ℝ) a < s
st : s < t
ht : ∀ b ∈ s_1, t < (f : (a : E) → ℝ) b
⊢ ∀ b ∈ t_1, -s < (-f : (a : E) → ℝ) b

Tactic:
simpa using hs
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : x ∉ t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (f : (a : E) → ℝ) x < u ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
let ⟨f, _u, v, ha, hst, hb⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton ht₁ ht₂
      (disjoint_singleton_left.2 disj)
  ⟨f, v, hst.trans' <| ha x <| mem_singleton _, hb⟩

Premises used: Iff.mpr, Set.mem_singleton, geometric_hahn_banach_compact_closed, _private.0.geometric_hahn_banach_point_closed.match_1, Set.disjoint_singleton_left, convex_singleton, Exists, LT.lt.trans', isCompact_singleton, And, And.intro, LT.lt, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
disj : x ∉ s
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < (f : (a : E) → ℝ) x

Tactic:
let ⟨f, s, _t, ha, hst, hb⟩ :=
    geometric_hahn_banach_closed_compact hs₁ hs₂ (convex_singleton x) isCompact_singleton
      (disjoint_singleton_right.2 disj)
  ⟨f, s, ha, hst.trans <| hb x <| mem_singleton _⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.disjoint_singleton_right, convex_singleton, Exists, geometric_hahn_banach_closed_compact, isCompact_singleton, And, _private.0.geometric_hahn_banach_closed_point.match_1, And.intro, LT.lt, Exists.intro, LT.lt.trans, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x y : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : T1Space E
hxy : x ≠ y
obtain :
  ∀ (f : StrongDual ℝ E) (s t : ℝ) (hs : ∀ (a : E), Membership.mem (γ := Set E) {x} a → (f : (a : E) → ℝ) a < s)
    (st : s < t) (ht : ∀ (b : E), Membership.mem (γ := Set E) {y} b → t < (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual ℝ E), LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)
⊢ ∃ (f : StrongDual ℝ E), LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)

Tactic:
obtain ⟨f, s, t, hs, st, ht⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton
      (convex_singleton y) isClosed_singleton (disjoint_singleton.2 hxy)

Premises used: Iff.mpr, geometric_hahn_banach_compact_closed, convex_singleton, Set.disjoint_singleton, isCompact_singleton, isClosed_singleton
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x y : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : T1Space E
hxy : x ≠ y
f : StrongDual ℝ E
s t : ℝ
hs : ∀ (a : E), Membership.mem (γ := Set E) {x} a → (f : (a : E) → ℝ) a < s
st : s < t
ht : ∀ (b : E), Membership.mem (γ := Set E) {y} b → t < (f : (a : E) → ℝ) b
linarith :
  LE.le (α := ℝ) ((f : (a : E) → ℝ) y : ℝ) ((f : (a : E) → ℝ) x : ℝ) →
    s - t + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) y : ℝ) ((f : (a : E) → ℝ) x : ℝ) +
          HSub.hSub (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) s +
        HSub.hSub (β := ℝ) t ((f : (a : E) → ℝ) y : ℝ) =
      0
⊢ LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)

Tactic:
linarith [hs x rfl, ht y rfl]

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x y : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : T1Space E
hxy : x ≠ y
f : StrongDual ℝ E
s t : ℝ
hs : ∀ (a : E), Membership.mem (γ := Set E) {x} a → (f : (a : E) → ℝ) a < s
st : s < t
ht : ∀ (b : E), Membership.mem (γ := Set E) {y} b → t < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E), LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)

Tactic:
exact ⟨f, by linarith [hs x rfl, ht y 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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
rw : {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} = s
⊢ ⋂ (l : StrongDual ℝ E), {x : E | ∃ y ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)} = s

Tactic:
rw [Set.iInter_setOf]

Premises used: Set.iInter_setOf
-- 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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} = s

Tactic:
Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_rfl⟩

Premises used: Set.Subset.antisymm, le_rfl, 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 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
refine :
  ∀ (x : E)
    (hx :
      Membership.mem (γ := Set E)
        {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)}
        x),
    x ∈ s
⊢ {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} = s

Tactic:
refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} x
by_contra : ∀ (h : x ∉ s), False
⊢ x ∈ s

Tactic:
by_contra h
-- 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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} x
h : x ∉ s
obtain :
  ∀ (l : StrongDual ℝ E) (s_1 : ℝ) (hlA : ∀ a ∈ s, (l : (a : E) → ℝ) a < s_1) (hl : s_1 < (l : (a : E) → ℝ) x), False
⊢ False

Tactic:
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point hs₁ hs₂ h

Premises used: geometric_hahn_banach_closed_point
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s_1, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} x
h : x ∉ s_1
l : StrongDual ℝ E
s : ℝ
hlA : ∀ a ∈ s_1, (l : (a : E) → ℝ) a < s
hl : s < (l : (a : E) → ℝ) x
obtain : ∀ (y : E) (hy : y ∈ s_1) (hxy : LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)), False
⊢ False

Tactic:
obtain ⟨y, hy, hxy⟩ := hx l
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s_1, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} x
h : x ∉ s_1
l : StrongDual ℝ E
s : ℝ
hlA : ∀ a ∈ s_1, (l : (a : E) → ℝ) a < s
hl : s < (l : (a : E) → ℝ) x
y : E
hy : y ∈ s_1
hxy : LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)
⊢ False

Tactic:
((hxy.trans_lt (hlA y hy)).trans hl).not_ge le_rfl

Premises used: le_rfl, LT.lt.trans, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsClosed s_1
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s_1, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} x
h : x ∉ s_1
l : StrongDual ℝ E
s : ℝ
hlA : ∀ a ∈ s_1, (l : (a : E) → ℝ) a < s
hl : s < (l : (a : E) → ℝ) x
y : E
hy : y ∈ s_1
hxy : LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)
⊢ False

Tactic:
exact ((hxy.trans_lt (hlA y hy)).trans hl).not_ge le_rfl

Premises used: le_rfl, LT.lt.trans, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
⊢ ContinuousSMul ℝ E

Tactic:
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
this : ContinuousSMul ℝ E
obtain :
  ∀ (g : StrongDual ℝ E)
    (hg : Eq (α := ℝ) ((g : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((g : (a : E) → ℝ) x : ℝ) (1 : ℝ)),
    ∃ (f : StrongDual 𝕜 E),
      Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
        ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
      ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)

Tactic:
obtain ⟨g, hg⟩ := _root_.separate_convex_open_set hs₀ hs₁ hs₂ hx₀

Premises used: separate_convex_open_set
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
hg : Eq (α := ℝ) ((g : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((g : (a : E) → ℝ) x : ℝ) (1 : ℝ)
h :
  Eq (α := ℝ)
      ((re : (a : 𝕜) → ℝ)
          ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜) x₀ :
            𝕜) :
        ℝ)
      (1 : ℝ) ∧
    ∀ x ∈ s,
      LT.lt (α := ℝ)
        ((re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜) x :
              𝕜) :
          ℝ)
        (1 : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
      ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)

Tactic:
use g.extendRCLikeₗ

Premises used: StrongDual.extendRCLikeₗ, DFunLike.coe