awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2
have linarith₁ : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2
have linarith₂ : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 < u
have linarith : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 < u
have linarith₁ : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 < u
have linarith₂ : u ≤ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 < u
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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), LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)
have 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 : ℝ)
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:
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
⊢ LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) y : ℝ)
have 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
Tactic: linarith [hs x rfl, ht y rfl]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ⋂ (l : StrongDual ℝ E), {x : E | ∃ y ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)} = s
have rw : {x : E | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, LE.le (α := ℝ) ((i : (a : E) → ℝ) x : ℝ) ((i : (a : E) → ℝ) y : ℝ)} = s
Tactic: rw [Set.iInter_setOf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
have 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
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:
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
⊢ x ∈ s
have by_contra : ∀ (h : x ∉ s), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ False
have obtain : ∀ (l : StrongDual ℝ E) (s_1 : ℝ) (hlA : ∀ a ∈ s, (l : (a : E) → ℝ) a < s_1) (hl : s_1 < (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:
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
⊢ False
have obtain : ∀ (y : E) (hy : y ∈ s_1) (hxy : LE.le (α := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ)), False
Tactic: obtain ⟨y, hy, hxy⟩ := hx l
-- 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
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
⊢ ∃ (f : StrongDual 𝕜 E),
    Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
      ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)
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
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
⊢ ∃ (f : StrongDual 𝕜 E),
    Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
      ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨g, hg⟩ := _root_.separate_convex_open_set hs₀ hs₁ hs₂ hx₀
-- 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
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 : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x₀ : 𝕜) : ℝ) (1 : ℝ) ∧
      ∀ x ∈ s, LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: use g.extendRCLikeₗ
-- 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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ 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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
this : ContinuousSMul ℝ E
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open hs₁ hs₂ 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
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
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u ≤ (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 :
            𝕜)
Tactic: use f.extendRCLikeₗ
-- 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 : 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
⊢ ∃ (f : StrongDual 𝕜 E),
    ∀ a ∈ s,
      LT.lt (α := ℝ) ((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
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),
    ∀ a ∈ s,
      LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
have 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 : 𝕜) : ℝ)
Tactic: obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ 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 : 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 : ℝ)
⊢ ∃ (f : StrongDual 𝕜 E),
    ∀ a ∈ s,
      LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) : ℝ)
        ((re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
have 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 :
          𝕜) :
      ℝ)
Tactic: use f.extendRCLikeₗ
-- 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
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ 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
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
this : ContinuousSMul ℝ E
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 : 𝕜)
Tactic: obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open_open 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
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
⊢ ∃ (f : StrongDual 𝕜 E) (u : ℝ),
    (∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u) ∧
      ∀ b ∈ t, u < (re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) b : 𝕜)
have 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 :
            𝕜)
Tactic: use f.extendRCLikeₗ