awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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 : 𝕜)
have this : ContinuousSMul ℝ E
Tactic: have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: obtain ⟨f, u, hfne, hA', hB'⟩ :=
    _root_.geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜)
have refine_1 : ∀
  (hzero :
    Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
      (0 : StrongDual 𝕜 E)),
  False
Tactic: refine ⟨f.extendRCLikeₗ, u, fun hzero ↦ ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have refine_2 : ∀ a ∈ s,
  (re : (a : 𝕜) → ℝ)
      ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) a : 𝕜) ≤
    u
Tactic: refine ⟨f.extendRCLikeₗ, u, fun hzero ↦ ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    f ≠ 0 ∧
      (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
        ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have refine_3 : ∀ b ∈ t,
  u ≤
    (re : (a : 𝕜) → ℝ)
      ((((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜) b : 𝕜)
Tactic: refine ⟨f.extendRCLikeₗ, u, fun hzero ↦ ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: by_cases htne : t.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: by_cases htne : t.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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 : 𝕜)
have 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 : 𝕜)
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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜)
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) ≤ u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: obtain ⟨f, u, -, hs', ht'⟩ := hsep
Cleared hypotheses: hsep
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
⊢ ∃ (f : StrongDual 𝕜 E),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
have this : ContinuousSMul ℝ E
Tactic: have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
have 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 : 𝕜) : ℝ)
Tactic: obtain ⟨f, hfne, hA'⟩ := _root_.geometric_hahn_banach_of_nonempty_interior_point hA hxA hAint
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜) : ℝ)
have refine_1 : ∀
  (hzero :
    Eq (α := StrongDual 𝕜 E) ((StrongDual.extendRCLikeₗ : (a : StrongDual ℝ E) → StrongDual 𝕜 E) f : StrongDual 𝕜 E)
      (0 : StrongDual 𝕜 E)),
  False
Tactic: refine ⟨f.extendRCLikeₗ, fun hzero ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual 𝕜 E),
    f ≠ 0 ∧
      ∀ a ∈ A,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
have 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 :
          𝕜) :
      ℝ)
Tactic: refine ⟨f.extendRCLikeₗ, fun hzero ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
⊢ ∃ (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 : 𝕜)
have this : ContinuousSMul ℝ E
Tactic: have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (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 : 𝕜)
have 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 : 𝕜)
Tactic: obtain ⟨g, u, v, h1⟩ := _root_.geometric_hahn_banach_compact_closed hs₁ hs₂ ht₁ ht₂ disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (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 : 𝕜)
have 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 :
              𝕜)
Tactic: use g.extendRCLikeₗ
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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),
    LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ)
have 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 : 𝕜) : ℝ)
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)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜)
⊢ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) y : 𝕜) : ℝ)
have 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
Tactic: linarith [hs x rfl, ht y rfl]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ⋂ (l : StrongDual 𝕜 E),
      {x : E |
        ∃ y ∈ s,
          LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ)
            ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)} =
    s
have rw : {x : E |
    ∀ (i : StrongDual 𝕜 E),
      ∃ y ∈ s,
        LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) : ℝ)
          ((re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) : ℝ)} =
  s
Tactic: rw [Set.iInter_setOf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
have 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
Tactic: refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ x ∈ s
have by_contra : ∀ (h : x ∉ s), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ False
have 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
Tactic: obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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 : 𝕜)
⊢ False
have obtain : ∀ (y : E) (hy : y ∈ s_1)
  (hxy :
    LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ)
      ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)),
  False
Tactic: obtain ⟨y, hy, hxy⟩ := hx l
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ⋂ (l : StrongDual 𝕜 E),
      ⋂ (c : ℝ),
        ⋂ (_ : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c),
          {x : E | (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) ≤ c} =
    s
have simp_rw : {x : E |
    ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
      (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1} =
  s
Tactic: simp_rw [Set.iInter_setOf]