awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ (∀ a ∈ s, LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((0 : (a : E) → 𝕜) a : 𝕜) : ℝ) (0 : ℝ)) ∧
    ∀ b ∈ t, LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ((0 : (a : E) → 𝕜) b : 𝕜) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : 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, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
exact ⟨0, 0, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
⊢ 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
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual ℝ E) (hfne : f ≠ 0)
    (hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)),
    ∃ (f : StrongDual 𝕜 E),
      f ≠ 0 ∧
        ∀ a ∈ A,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)

Tactic:
obtain ⟨f, hfne, hA'⟩ := _root_.geometric_hahn_banach_of_nonempty_interior_point hA hxA hAint

Premises used: geometric_hahn_banach_of_nonempty_interior_point
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)

Tactic:
⟨f.extendRCLikeₗ, fun hzero ↦ ?_, ?_⟩

Premises used: And.intro, StrongDual.extendRCLikeₗ, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
refine_1 :
  ∀
    (hzero :
      Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
        (0 : StrongDual 𝕜 E)),
    False
refine_2 :
  ∀ a ∈ A,
    LE.le (α := ℝ)
      ((re : (a : 𝕜) → ℝ)
          ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
            𝕜) :
        ℝ)
      ((re : (a : 𝕜) → ℝ)
          ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) x :
            𝕜) :
        ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)

Tactic:
refine ⟨f.extendRCLikeₗ, fun hzero ↦ ?_, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
hzero :
  Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
    (0 : StrongDual 𝕜 E)
⊢ Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
    ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) 0 : StrongDual 𝕜 E)

Tactic:
simpa using hzero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
hzero :
  Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
    (0 : StrongDual 𝕜 E)
⊢ False

Tactic:
exact hfne <| (StrongDual.extendRCLikeₗ (𝕜 := 𝕜)).injective (by simpa using hzero)

Premises used: StrongDual.extendRCLikeₗ, LinearEquiv.injective
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∀ a ∈ A,
    LE.le (α := ℝ)
      ((re : (a : 𝕜) → ℝ)
          ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
            𝕜) :
        ℝ)
      ((re : (a : 𝕜) → ℝ)
          ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) x :
            𝕜) :
        ℝ)

Tactic:
simpa [f.extendRCLikeₗ_apply] using hA'

Premises used: StrongDual.extendRCLikeₗ_apply
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
⊢ 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
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
this : ContinuousSMul ℝ E
obtain :
  ∀ (g : StrongDual ℝ E) (u v : ℝ) (h1 : (∀ a ∈ s, (g : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (g : (a : E) → ℝ) b),
    ∃ (f : StrongDual 𝕜 E) (u : ℝ) (v : ℝ),
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
        u < v ∧ ∀ b ∈ t, v < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ) (v : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      u < v ∧ ∀ b ∈ t, v < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
obtain ⟨g, u, v, h1⟩ := _root_.geometric_hahn_banach_compact_closed hs₁ hs₂ ht₁ ht₂ disj

Premises used: geometric_hahn_banach_compact_closed
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
u v : ℝ
h1 : (∀ a ∈ s, (g : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (g : (a : E) → ℝ) b
h :
  ∃ (u : ℝ) (v : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      u < v ∧
        ∀ b ∈ t,
          v <
            (re : (a : 𝕜) → ℝ)
              ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜)
                  b :
                𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ) (v : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      u < v ∧ ∀ b ∈ t, v < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
use g.extendRCLikeₗ

Premises used: StrongDual.extendRCLikeₗ, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
u v : ℝ
h1 : (∀ a ∈ s, (g : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (g : (a : E) → ℝ) b
⊢ ∃ (u : ℝ) (v : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      u < v ∧
        ∀ b ∈ t,
          v <
            (re : (a : 𝕜) → ℝ)
              ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) g : StrongDual 𝕜 E) : (a : E) → 𝕜)
                  b :
                𝕜)

Tactic:
simpa [g.extendRCLikeₗ_apply, exists_and_left] using ⟨u, h1.1, v, h1.2⟩

Premises used: exists_and_left, StrongDual.extendRCLikeₗ_apply
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : 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, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < s
st : s < t
ht : ∀ b ∈ s_1, t < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∀ a ∈ s_1, (re : (a : 𝕜) → ℝ) ((-f : (a : E) → 𝕜) a : 𝕜) < -t

Tactic:
simpa using ht
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : 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, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < s
st : s < t
ht : ∀ b ∈ s_1, t < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ -t < -s

Tactic:
simpa using st
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t_1 : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : 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, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < s
st : s < t
ht : ∀ b ∈ s_1, t < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∀ b ∈ t_1, -s < (re : (a : 𝕜) → ℝ) ((-f : (a : E) → 𝕜) b : 𝕜)

Tactic:
simpa using hs
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : x ∉ t
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) < u ∧ ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((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, _private.0.RCLike.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, RCLike.re, RCLike.geometric_hahn_banach_compact_closed, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
disj : x ∉ s
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧ u < (re : (a : 𝕜) → ℝ) ((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, isCompact_singleton, And, And.intro, LT.lt, Exists.intro, RCLike.re, LT.lt.trans, DFunLike.coe, _private.0.RCLike.geometric_hahn_banach_closed_point.match_1, RCLike.geometric_hahn_banach_closed_compact
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x y : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : T1Space E
hxy : x ≠ y
obtain :
  ∀ (f : StrongDual 𝕜 E) (s t : ℝ)
    (hs : ∀ (a : E), Membership.mem (γ := Set E) {x} a → (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < s) (st : s < t)
    (ht : ∀ (b : E), Membership.mem (γ := Set E) {y} b → t < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)),
    ∃ (f : StrongDual 𝕜 E),
      LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((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, convex_singleton, Set.disjoint_singleton, isCompact_singleton, RCLike.geometric_hahn_banach_compact_closed, isClosed_singleton
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x y : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : T1Space E
hxy : x ≠ y
f : StrongDual 𝕜 E
s t : ℝ
hs : ∀ (a : E), Membership.mem (γ := Set E) {x} a → (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < s
st : s < t
ht : ∀ (b : E), Membership.mem (γ := Set E) {y} b → t < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
linarith :
  LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) →
    s - t +
            HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ)
              ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) +
          HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) s +
        HSub.hSub (β := ℝ) t ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ) =
      0
⊢ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ)

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

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

Tactic:
exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
rw :
  {x : E |
      ∀ (i : StrongDual 𝕜 E),
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) : ℝ)} =
    s
⊢ ⋂ (l : StrongDual 𝕜 E),
      {x : E |
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)} =
    s

Tactic:
rw [Set.iInter_setOf]

Premises used: Set.iInter_setOf
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x : E |
      ∀ (i : StrongDual 𝕜 E),
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((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:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : 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 (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
                ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) : ℝ)}
        x),
    x ∈ s
⊢ {x : E |
      ∀ (i : StrongDual 𝕜 E),
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((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:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E |
      ∀ (i : StrongDual 𝕜 E),
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) : ℝ)}
    x
by_contra : ∀ (h : x ∉ s), False
⊢ x ∈ s

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

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

Premises used: RCLike.geometric_hahn_banach_closed_point
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : 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 (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) : ℝ)}
    x
h : x ∉ s_1
l : StrongDual 𝕜 E
s : ℝ
hlA : ∀ a ∈ s_1, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) a : 𝕜) < s
hl : s < (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜)
obtain :
  ∀ (y : E) (hy : y ∈ s_1)
    (hxy :
      LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)),
    False
⊢ False

Tactic:
obtain ⟨y, hy, hxy⟩ := hx l