awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
F : Type u_4
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜₂ F
inst_4 : IsTopologicalAddGroup F
n : ℤ
x : F
⊢ ((↑n : F →WOT[𝕜₂] F) : (a : F) → F) x = n • x

Tactic:
rfl

Premises used: rfl
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x y : E →SWOT[σ] F
h :
  ∀ (x_1 : E × F⋆),
    (match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x + y : (a : E) → F) x_2 : F)) =
      HAdd.hAdd (α := E × F⋆ → 𝕜₂) (β := E × F⋆ → 𝕜₂)
        (fun (x_2 : E × F⋆) ↦
          match (motive := E × F⋆ → 𝕜₂) x_2 with
          | (x_3, y) => (y : (a : F) → 𝕜₂) ((x : (a : E) → F) x_3 : F))
        (fun (x : E × F⋆) ↦
          match (motive := E × F⋆ → 𝕜₂) x with
          | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
        x_1
⊢ (fun (x_1 : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x + y : (a : E) → F) x_2 : F)) =
    HAdd.hAdd (α := E × F⋆ → 𝕜₂)
      (fun (x_1 : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x_1 with
        | (x_2, y) => (y : (a : F) → 𝕜₂) ((x : (a : E) → F) x_2 : F))
      fun (x : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x with
      | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F)

Tactic:
ext
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x y : E →SWOT[σ] F
x_1 : E × F⋆
⊢ (match (motive := E × F⋆ → 𝕜₂) x_1 with
    | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x + y : (a : E) → F) x_2 : F)) =
    HAdd.hAdd (α := E × F⋆ → 𝕜₂) (β := E × F⋆ → 𝕜₂)
      (fun (x_2 : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x_2 with
        | (x_3, y) => (y : (a : F) → 𝕜₂) ((x : (a : E) → F) x_3 : F))
      (fun (x : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x with
        | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
      x_1

Tactic:
simp
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
h :
  ∀ (x_1 : E × F⋆),
    (match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x • y : (a : E) → F) x_2 : F)) =
      HSMul.hSMul (α := 𝕜₂) (β := E × F⋆ → 𝕜₂) ((RingHom.id 𝕜₂ : (a : 𝕜₂) → 𝕜₂) x : 𝕜₂)
        (fun (x : E × F⋆) ↦
          match (motive := E × F⋆ → 𝕜₂) x with
          | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
        x_1
⊢ (fun (x_1 : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x • y : (a : E) → F) x_2 : F)) =
    HSMul.hSMul (α := 𝕜₂) (β := E × F⋆ → 𝕜₂) ((RingHom.id 𝕜₂ : (a : 𝕜₂) → 𝕜₂) x : 𝕜₂) fun (x : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x with
      | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F)

Tactic:
ext
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
x_1 : E × F⋆
⊢ (match (motive := E × F⋆ → 𝕜₂) x_1 with
    | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x • y : (a : E) → F) x_2 : F)) =
    HSMul.hSMul (α := 𝕜₂) (β := E × F⋆ → 𝕜₂) ((RingHom.id 𝕜₂ : (a : 𝕜₂) → 𝕜₂) x : 𝕜₂)
      (fun (x : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x with
        | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
      x_1

Tactic:
simp
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
f : E →SWOT[σ] F
x : E
y : F⋆
⊢ Eq.{u_2 + 1} (α := 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) f (x, y) : 𝕜₂)
    ((y : (a : F) → 𝕜₂) ((f : (a : E) → F) x : F) : 𝕜₂)

Tactic:
rfl

Premises used: rfl
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
⊢ Continuous[instTopologicalSpace, Pi.topologicalSpace] (⇑(inducingFn σ E F) : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂)

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (A : E →SWOT[σ] F) ↦
    (y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F)

Tactic:
(continuous_pi_iff.mp continuous_inducingFn) ⟨x, y⟩

Premises used: Prod.mk, continuous_pi_iff, Iff.mp, ContinuousLinearMapWOT.continuous_inducingFn
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (A : E →SWOT[σ] F) ↦
    (y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F)

Tactic:
refine (continuous_pi_iff.mp continuous_inducingFn) ⟨x, y⟩

Premises used: Prod.mk, continuous_pi_iff, Iff.mp, ContinuousLinearMapWOT.continuous_inducingFn
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
α : Type u_5
inst_10 : TopologicalSpace α
g : α → E →SWOT[σ] F
h :
  ∀ (x : E) (y : F⋆),
    Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : α) ↦
      (y : (a : F) → 𝕜₂) ((g a : (a : E) → F) x : F)
⊢ Continuous[inst_10, instTopologicalSpace] g

Tactic:
continuous_induced_rng.2 (continuous_pi_iff.mpr fun p => h p.1 p.2)

Premises used: Iff.mpr, Prod.fst, continuous_pi_iff, Prod.snd, continuous_induced_rng
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
⊢ IsInducing (X := E →SWOT[σ] F) (Y := E × F⋆ → 𝕜₂) (⇑(inducingFn σ E F) : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂)

Tactic:
⟨rfl⟩

Premises used: Topology.IsInducing.mk, rfl
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
⊢ IsEmbedding (X := E →SWOT[σ] F) (Y := E × F⋆ → 𝕜₂) (⇑(inducingFn σ E F) : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂)

Tactic:
Function.Injective.isEmbedding_induced fun A B hAB => ?_

Premises used: Function.Injective.isEmbedding_induced
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
refine :
  ∀ (A B : E →SWOT[σ] F)
    (hAB :
      Eq (α := E × F⋆ → 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) A : E × F⋆ → 𝕜₂)
        ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) B : E × F⋆ → 𝕜₂)),
    A = B
⊢ IsEmbedding (X := E →SWOT[σ] F) (Y := E × F⋆ → 𝕜₂) (⇑(inducingFn σ E F) : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂)

Tactic:
refine Function.Injective.isEmbedding_induced fun A B hAB => ?_

Premises used: Function.Injective.isEmbedding_induced
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
hAB :
  Eq (α := E × F⋆ → 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) A : E × F⋆ → 𝕜₂)
    ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) B : E × F⋆ → 𝕜₂)
rw :
  ∀ (x : E) (y : F⋆),
    Eq.{u_2 + 1} (α := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)
      ((y : (a : F) → 𝕜₂) ((B : (a : E) → F) x : F) : 𝕜₂)
⊢ A = B

Tactic:
rw [ContinuousLinearMapWOT.ext_dual_iff]

Premises used: ContinuousLinearMapWOT.ext_dual_iff
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
hAB :
  Eq (α := E × F⋆ → 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) A : E × F⋆ → 𝕜₂)
    ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) B : E × F⋆ → 𝕜₂)
⊢ ∀ (x : E) (y : F⋆),
    Eq.{u_2 + 1} (α := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)
      ((y : (a : F) → 𝕜₂) ((B : (a : E) → F) x : F) : 𝕜₂)

Tactic:
simpa [funext_iff] using hAB

Premises used: funext_iff
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
α : Type u_5
l : Filter α
f : α → E →SWOT[σ] F
A : E →SWOT[σ] F
⊢ Tendsto f l (𝓝 A) ↔
    ∀ (x : E) (y : F⋆),
      Tendsto.{u_5, u_2} (β := 𝕜₂) (fun (a : α) ↦ ((y : (a : F) → 𝕜₂) ((f a : (a : E) → F) x : F) : 𝕜₂)) l
        (𝓝 ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F)) : Filter 𝕜₂)

Tactic:
simp [isInducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]

Premises used: ContinuousLinearMapWOT.isInducing_inducingFn, tendsto_pi_nhds, Topology.IsInducing.tendsto_nhds_iff
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
l : Filter (E →SWOT[σ] F)
A : E →SWOT[σ] F
⊢ l ≤ 𝓝 A ↔
    ∀ (x : E) (y : F⋆),
      LE.le.{u_2} (α := Filter 𝕜₂)
        (Filter.map (fun (T : E →SWOT[σ] F) ↦ (y : (a : F) → 𝕜₂) ((T : (a : E) → F) x : F)) l : Filter 𝕜₂)
        (𝓝 ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F)) : Filter 𝕜₂)

Tactic:
tendsto_iff_forall_dual_apply_tendsto (f := id)

Premises used: Set.Mem, setOf, Set.preimage, Filter.Tendsto, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
⊢ T3Space (E →SWOT[σ] F)

Tactic:
isEmbedding_inducingFn.t3Space

Premises used: ContinuousLinearMapWOT.isEmbedding_inducingFn, Topology.IsEmbedding.t3Space
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
apply :
  ∀ (x : F) (x_1 : F⋆),
    Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
      (x_1 : (a : F) → 𝕜₂) ((c • a : (a : F) → F) x : F)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x : F →WOT[𝕜₂] F) ↦ c • x

Tactic:
apply continuous_of_dual_apply_continuous fun _ _ ↦ ?_

Premises used: ContinuousLinearMapWOT.continuous_of_dual_apply_continuous
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
x : F
x_1 : F⋆
simp :
  Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    HSMul.hSMul (β := 𝕜₂) c ((x_1 : (a : F) → 𝕜₂) ((a : (a : F) → F) x : F) : 𝕜₂)
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    (x_1 : (a : F) → 𝕜₂) ((c • a : (a : F) → F) x : F)

Tactic:
simp only [smul_apply, ContinuousLinearMap.map_smul_of_tower]

Premises used: ContinuousLinearMap.map_smul_of_tower, ContinuousLinearMapWOT.smul_apply
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
x : F
x_1 : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    HSMul.hSMul (β := 𝕜₂) c ((x_1 : (a : F) → 𝕜₂) ((a : (a : F) → F) x : F) : 𝕜₂)

Tactic:
continuous_const_smul c |>.comp <| continuous_dual_apply ..

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, ContinuousLinearMapWOT.continuous_dual_apply
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
x : F
x_1 : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    HSMul.hSMul (β := 𝕜₂) c ((x_1 : (a : F) → 𝕜₂) ((a : (a : F) → F) x : F) : 𝕜₂)

Tactic:
exact continuous_const_smul c |>.comp <| continuous_dual_apply ..

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, ContinuousLinearMapWOT.continuous_dual_apply
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : Semiring S
inst_11 : Module S F
inst_12 : SMulCommClass 𝕜₂ S F
inst_13 : Module S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ F
inst_15 : IsScalarTower S 𝕜₂ 𝕜₂
inst_16 : ContinuousConstSMul S F
inst_17 : TopologicalSpace S
inst_18 : ContinuousSMul S 𝕜₂
⊢ ContinuousSMul S (E →SWOT[σ] F)

Tactic:
.induced <| (inducingFn σ E F).restrictScalars S

Premises used: LinearMap.restrictScalars, ContinuousLinearMapWOT.inducingFn, ContinuousSMul.induced
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
⊢ IsUniformAddGroup (E →SWOT[σ] F)

Tactic:
.comap (inducingFn σ E F)

Premises used: IsUniformAddGroup.comap, ContinuousLinearMapWOT.inducingFn
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
⊢ norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((0 : (a : E) → F) x : F) : 𝕜₂) = 0

Tactic:
simp
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
A B : E →SWOT[σ] F
⊢ norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A + B : (a : E) → F) x : F) : 𝕜₂) ≤
    norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂) +
      norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((B : (a : E) → F) x : F) : 𝕜₂)

Tactic:
simpa using norm_add_le _ _

Premises used: norm_add_le
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
A : E →SWOT[σ] F
⊢ norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((-A : (a : E) → F) x : F) : 𝕜₂) =
    norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)

Tactic:
simp
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
r : 𝕜₂
A : E →SWOT[σ] F
⊢ norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((r • A : (a : E) → F) x : F) : 𝕜₂) =
    ‖r‖ * norm.{u_2} (E := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)

Tactic:
simp
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
⊢ WithSeminorms (E := E →SWOT[σ] F) (seminormFamily σ E F)

Tactic:
let e : E × F⋆ ≃ (Σ _ : E × F⋆, Fin 1) := .symm <| .sigmaUnique _ _
  isInducing_inducingFn.withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜₂ 𝕜₂)
    |>.congr_equiv e

Premises used: SeminormFamily.comp, ContinuousLinearMapWOT.isInducing_inducingFn, WithSeminorms.congr_equiv, Topology.IsInducing.withSeminorms, withSeminorms_pi, norm_withSeminorms, ContinuousLinearMapWOT.seminormFamily, Seminorm.comp, Equiv.symm, Prod, OfNat.ofNat, Fin, StrongDual, Equiv.sigmaUnique, ContinuousLinearMapWOT.seminorm
-- 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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
⊢ Filter.HasBasis (𝓝 0)
    (fun (x : Set (E →SWOT[σ] F)) ↦
      Membership.mem (γ := Set (Set (E →SWOT[σ] F))) (SeminormFamily.basisSets (seminormFamily σ E F)) x)
    id

Tactic:
withSeminorms.hasBasis

Premises used: ContinuousLinearMapWOT.withSeminorms, Set.Mem, WithSeminorms.hasBasis