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
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 : ℝ)
⊢ 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 : ℝ)

Tactic:
simpa [g.extendRCLikeₗ_apply]

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
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ 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
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual 𝕜 E) (u : ℝ),
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open hs₁ hs₂ ht disj

Premises used: geometric_hahn_banach_open
-- 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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
h₁ :
  ∃ (u : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      ∀ b ∈ t,
        u ≤
          (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b :
              𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
use f.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
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (u : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      ∀ b ∈ t,
        u ≤
          (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b :
              𝕜)

Tactic:
simpa [f.extendRCLikeₗ_apply] using Exists.intro u h

Premises used: StrongDual.extendRCLikeₗ_apply, 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
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : 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
s : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual ℝ E) (h : ∀ a ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)),
    ∃ (f : StrongDual 𝕜 E),
      ∀ a ∈ s,
        LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    ∀ a ∈ s,
      LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)

Tactic:
obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ disj

Premises used: geometric_hahn_banach_open_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 : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
h : ∀ a ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
h₁ :
  ∀ a ∈ s,
    LT.lt (α := ℝ)
      ((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),
    ∀ a ∈ s,
      LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)

Tactic:
use f.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 : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
h : ∀ a ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∀ a ∈ s,
    LT.lt (α := ℝ)
      ((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]

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
t : Set E
x : E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : x ∉ t
f : StrongDual 𝕜 E
hf :
  ∀ a ∈ t,
    LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
⊢ ∀ b ∈ t,
    LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((-f : (a : E) → 𝕜) x : 𝕜) : ℝ)
      ((re : (a : 𝕜) → ℝ) ((-f : (a : E) → 𝕜) b : 𝕜) : ℝ)

Tactic:
simpa
-- 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
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen 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
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual 𝕜 E) (u : ℝ),
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
        ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open_open hs₁ hs₂ ht₁ ht₃ disj

Premises used: geometric_hahn_banach_open_open
-- 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
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
h₁ :
  ∃ (u : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      ∀ b ∈ t,
        u <
          (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b :
              𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
use f.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
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
h : (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
⊢ ∃ (u : ℝ),
    (∀ a ∈ s,
        (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
              𝕜) <
          u) ∧
      ∀ b ∈ t,
        u <
          (re : (a : 𝕜) → ℝ)
            ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b :
              𝕜)

Tactic:
simpa [f.extendRCLikeₗ_apply] using Exists.intro u h

Premises used: StrongDual.extendRCLikeₗ_apply, 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 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
⊢ 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
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual ℝ E) (u : ℝ) (hfne : f ≠ 0) (hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u)
    (hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b),
    ∃ (f : StrongDual 𝕜 E) (u : ℝ),
      f ≠ 0 ∧
        (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
          ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
obtain ⟨f, u, hfne, hA', hB'⟩ :=
    _root_.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:
𝕜 : 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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
⟨f.extendRCLikeₗ, u, 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
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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
refine_1 :
  ∀
    (hzero :
      Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
        (0 : StrongDual 𝕜 E)),
    False
refine_2 :
  ∀ a ∈ s,
    (re : (a : 𝕜) → ℝ)
        ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
          𝕜) ≤
      u
refine_3 :
  ∀ b ∈ t,
    u ≤
      (re : (a : 𝕜) → ℝ)
        ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
refine ⟨f.extendRCLikeₗ, u, 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
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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
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
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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
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
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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∀ a ∈ s,
    (re : (a : 𝕜) → ℝ)
        ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a :
          𝕜) ≤
      u

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
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u
hB' : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∀ b ∈ t,
    u ≤
      (re : (a : 𝕜) → ℝ)
        ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b : 𝕜)

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

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
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, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
neg :
  ∀ (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 : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
by_cases htne : t.Nonempty

Premises used: Set.Nonempty
-- 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 : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
have hsep :
        ∃ (f : StrongDual 𝕜 E) (u : ℝ),
          f ≠ 0 ∧ (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b) :=
        geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
-- 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
hsep :
  ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
pos :
  ∀ (f : StrongDual 𝕜 E) (u : ℝ) (hs' : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u)
    (ht' : ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)),
    ∃ (f : StrongDual 𝕜 E) (u : ℝ),
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

Tactic:
obtain ⟨f, u, -, hs', ht'⟩ := hsep
-- 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 : ℝ
hs' : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u
ht' : ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

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

Premises used: 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 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 : ℝ
hs' : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u
ht' : ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)

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