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_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 : 𝕜)
y : E
hy : y ∈ s_1
hxy :
  LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)
⊢ False

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

Premises used: LT.lt.trans, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
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 : 𝕜)
y : E
hy : y ∈ s_1
hxy :
  LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) : ℝ)
⊢ False

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

Premises used: LT.lt.trans, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
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
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
⊢ ⋂ (l : StrongDual 𝕜 E),
      ⋂ (c : ℝ),
        ⋂ (_ : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c),
          {x : E | (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) ≤ c} =
    s

Tactic:
simp_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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1} =
    s

Tactic:
Set.Subset.antisymm (fun x hx => ?_) fun x hx l c hc => hc x hx

Premises used: Set.Subset.antisymm
-- 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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
            (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
        x),
    x ∈ s
⊢ {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:
refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l c hc => hc x hx
-- 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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    x
h : x ∉ s
obtain :
  ∀ (l : StrongDual 𝕜 E) (c : ℝ) (hls : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) a : 𝕜) < c)
    (hl : c < (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜)), False
⊢ False

Tactic:
obtain ⟨l, c, hls, 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 : 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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    x
h : x ∉ s
l : StrongDual 𝕜 E
c : ℝ
hls : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) a : 𝕜) < c
hl : c < (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜)
⊢ False

Tactic:
(hl.trans_le (hx l c (fun y hy ↦ (hls y hy).le))).false

Premises used: LT.lt.le, LT.lt.trans_le, LT.lt.false
-- 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) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    x
h : x ∉ s
l : StrongDual 𝕜 E
c : ℝ
hls : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) a : 𝕜) < c
hl : c < (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜)
⊢ False

Tactic:
exact (hl.trans_le (hx l c (fun y hy ↦ (hls y hy).le))).false

Premises used: LT.lt.le, LT.lt.trans_le, LT.lt.false
-- 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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
⊢ ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i

Tactic:
fun lc ↦ lc.2.prop

Premises used: Subtype.prop, Sigma.snd
-- 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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
x : E
h : x ∈ s
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ((0 : (a : E) → 𝕜) x : 𝕜) : ℝ) (0 : ℝ)

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 : 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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨0, 0, fun _ _ ↦ 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
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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this : Nonempty ι
⊢ ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s

Tactic:
simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ hs₂

Premises used: Set.iInter_subtype, RCLike.iInter_halfSpaces_eq', Set.iInter_sigma
-- 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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this : Nonempty ι
⊢ ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s

Tactic:
have : ⋂ i : ι, { x | re (l i x) ≤ c i } = s := by
    simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ 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
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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this_1 : Nonempty ι
this : ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s
obtain :
  ∀ (k : ℕ → ι)
    (hk :
      Eq.{u_2 + 1} (α := Set E) (⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l (k n) : (a : E) → 𝕜) x : 𝕜) ≤ c (k n)})
        (⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i})),
    ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ),
      ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s

Tactic:
obtain ⟨k, hk⟩ := eq_closed_inter_nat (fun i : ι ↦ { x | re (l i x) ≤ c i })
    (fun i ↦ isClosed_le (continuous_re.comp (l i).continuous) continuous_const)

Premises used: Continuous.comp, continuous_const, setOf, isClosed_le, LE.le, RCLike.continuous_re, ContinuousLinearMap.continuous, RCLike.re, eq_closed_inter_nat, 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
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 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this_1 : Nonempty ι
this : ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s
k : ℕ → ι
hk :
  Eq.{u_2 + 1} (α := Set E) (⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l (k n) : (a : E) → 𝕜) x : 𝕜) ≤ c (k n)})
    (⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i})
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s

Tactic:
⟨l ∘ k, c ∘ k, hk.trans this⟩

Premises used: Function.comp, Exists.intro, Eq.trans
-- 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
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this_1 : Nonempty ι
this : ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s
k : ℕ → ι
hk :
  Eq.{u_2 + 1} (α := Set E) (⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l (k n) : (a : E) → 𝕜) x : 𝕜) ≤ c (k n)})
    (⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i})
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s

Tactic:
exact ⟨l ∘ k, c ∘ k, hk.trans this⟩
-- Module: Mathlib.Analysis.LocallyConvex.StrongTopology
Goal:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : Module 𝕜₁ E
inst_10 : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module R F
inst_12 : ContinuousConstSMul R F
inst_13 : LocallyConvexSpace R F
inst_14 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
apply :
  ∀ (i : Prod.{u_4, u_5} (Set E) (Set F)),
    i.1 ∈ 𝔖 ∧ Membership.mem (γ := Filter F) (𝓝 0) i.2 ∧ Convex R i.2 →
      Convex R (E := UniformConvergenceCLM σ F 𝔖)
        {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ i.1, Membership.mem (α := F) (id i.2) ((f : (a : E) → F) x : F)}
⊢ LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)

Tactic:
apply LocallyConvexSpace.ofBasisZero _ _ _ _
    (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
      (LocallyConvexSpace.convex_basis_zero R F)) _

Premises used: LocallyConvexSpace.convex_basis_zero, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, LocallyConvexSpace.ofBasisZero
-- Module: Mathlib.Analysis.LocallyConvex.StrongTopology
Goal:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : Module 𝕜₁ E
inst_10 : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module R F
inst_12 : ContinuousConstSMul R F
inst_13 : LocallyConvexSpace R F
inst_14 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
S : Set E
V : Set F
left : (S, V).1 ∈ 𝔖
left_1 : Membership.mem (γ := Filter F) (𝓝 0) (S, V).2
hVconvex : Convex R (S, V).2
f : UniformConvergenceCLM σ F 𝔖
hf :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ (S, V).1, Membership.mem (α := F) (id (S, V).2) ((f : (a : E) → F) x : F)}
    f
g : UniformConvergenceCLM σ F 𝔖
hg :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ (S, V).1, Membership.mem (α := F) (id (S, V).2) ((f : (a : E) → F) x : F)}
    g
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : E
hx : x ∈ (S, V).1
⊢ Membership.mem (α := F) (id (S, V).2) ((a • f + b • g : (a : E) → F) x : F)

Tactic:
hVconvex (hf x hx) (hg x hx) ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Analysis.LocallyConvex.StrongTopology
Goal:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : Module 𝕜₁ E
inst_10 : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module R F
inst_12 : ContinuousConstSMul R F
inst_13 : LocallyConvexSpace R F
inst_14 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
S : Set E
V : Set F
left : (S, V).1 ∈ 𝔖
left_1 : Membership.mem (γ := Filter F) (𝓝 0) (S, V).2
hVconvex : Convex R (S, V).2
f : UniformConvergenceCLM σ F 𝔖
hf :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ (S, V).1, Membership.mem (α := F) (id (S, V).2) ((f : (a : E) → F) x : F)}
    f
g : UniformConvergenceCLM σ F 𝔖
hg :
  Membership.mem (γ := Set (UniformConvergenceCLM σ F 𝔖))
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ (S, V).1, Membership.mem (α := F) (id (S, V).2) ((f : (a : E) → F) x : F)}
    g
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : E
hx : x ∈ (S, V).1
⊢ Membership.mem (α := F) (id (S, V).2) ((a • f + b • g : (a : E) → F) x : F)

Tactic:
exact hVconvex (hf x hx) (hg x hx) ha hb hab
-- Module: Mathlib.Analysis.LocallyConvex.StrongTopology
Goal:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : Module 𝕜₁ E
inst_10 : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module R F
inst_12 : ContinuousConstSMul R F
inst_13 : LocallyConvexSpace R F
inst_14 : SMulCommClass 𝕜₂ R F
⊢ LocallyConvexSpace R (E →SL[σ] F)

Tactic:
UniformConvergenceCLM.locallyConvexSpace R _ ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
    (directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union)

Premises used: Bornology.isVonNBounded_empty, directedOn_of_sup_mem, Exists.intro, EmptyCollection.emptyCollection, UniformConvergenceCLM, Bornology.IsVonNBounded.union, UniformConvergenceCLM.locallyConvexSpace
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
⊢ Function.Injective (α := E →SWOT[σ] F) toCLM

Tactic:
equiv.injective

Premises used: Equiv.injective, ContinuousLinearMapWOT.equiv
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
⊢ Function.Surjective (α := E →SWOT[σ] F) toCLM

Tactic:
equiv.surjective

Premises used: Equiv.surjective, ContinuousLinearMapWOT.equiv
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
⊢ Function.Bijective (α := E →SWOT[σ] F) toCLM

Tactic:
equiv.bijective

Premises used: Equiv.bijective, ContinuousLinearMapWOT.equiv