awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 →SL[σ] F) ofCLM

Tactic:
equiv.symm.injective

Premises used: Equiv.injective, Equiv.symm, 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 →SL[σ] F) ofCLM

Tactic:
equiv.symm.surjective

Premises used: Equiv.surjective, Equiv.symm, 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 →SL[σ] F) ofCLM

Tactic:
equiv.symm.bijective

Premises used: Equiv.bijective, Equiv.symm, 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
S : Type u_5
T : Type u_6
inst_8 : DistribSMul S F
inst_9 : SMulCommClass 𝕜₂ S F
inst_10 : ContinuousConstSMul S F
inst_11 : DistribSMul T F
inst_12 : SMulCommClass 𝕜₂ T F
inst_13 : ContinuousConstSMul T F
inst_14 : SMul S T
inst_15 : IsScalarTower S T F
⊢ IsScalarTower S T (E →SWOT[σ] F)

Tactic:
equiv.isScalarTower S T

Premises used: Equiv.isScalarTower, 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
S : Type u_5
T : Type u_6
inst_8 : DistribSMul S F
inst_9 : SMulCommClass 𝕜₂ S F
inst_10 : ContinuousConstSMul S F
inst_11 : DistribSMul T F
inst_12 : SMulCommClass 𝕜₂ T F
inst_13 : ContinuousConstSMul T F
inst_14 : SMulCommClass S T F
⊢ SMulCommClass S T (E →SWOT[σ] F)

Tactic:
equiv.smulCommClass S T

Premises used: Equiv.smulCommClass, 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
S : Type u_5
inst_8 : Semiring S
inst_9 : Module S F
inst_10 : SMulCommClass 𝕜₂ S F
inst_11 : ContinuousConstSMul S F
inst_12 : Module.{u_5, u_4} Sᵐᵒᵖ F
inst_13 : IsCentralScalar S F
⊢ IsCentralScalar S (E →SWOT[σ] F)

Tactic:
equiv.isCentralScalar S

Premises used: Equiv.isCentralScalar, 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
A : E →SWOT[σ] F
⊢ Eq (α := (a : E) → F) (⇑A.toCLM : (a : E) → F) (⇑A : (a : E) → 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
A : E →SL[σ] F
⊢ Eq (α := (a : E) → F) (⇑(ofCLM A) : (a : E) → F) (⇑A : (a : E) → 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
f : E →SWOT[σ] F
x y : E
⊢ (f : (a : E) → F) (x + y) = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)

Tactic:
simp [← coe_toCLM]

Premises used: ContinuousLinearMapWOT.coe_toCLM
-- 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
f : E →SWOT[σ] F
r : 𝕜₁
x : E
⊢ (f : (a : E) → F) (r • x) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) (β := F) ((σ : (a : 𝕜₁) → 𝕜₂) r : 𝕜₂) ((f : (a : E) → F) x : F)

Tactic:
simp [← coe_toCLM]

Premises used: ContinuousLinearMapWOT.coe_toCLM
-- 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
A : E →SWOT[σ] F
⊢ ofCLM A.toCLM = A

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
A : E →SL[σ] F
⊢ (ofCLM A).toCLM = A

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
A : E →SWOT[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F) ((A.toCLM : (a : E) → F) x : F) ((A : (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
A : E →SL[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F) ((ofCLM A : (a : E) → F) x : F) ((A : (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
A B : E →SWOT[σ] F
h : ∀ (x : E), Eq.{u_4 + 1} (α := F) ((A : (a : E) → F) x : F) ((B : (a : E) → F) x : F)
⊢ A = B

Tactic:
toCLM_injective <| ContinuousLinearMap.ext h

Premises used: ContinuousLinearMapWOT.toCLM_injective, ContinuousLinearMap.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
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h :
  ∀ (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) : 𝕜₂)
simp_rw :
  ∀ (x : E) (x_1 : F →L[𝕜₂] 𝕜₂),
    Eq.{u_2 + 1} (α := 𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((A : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((B : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)
⊢ A = B

Tactic:
simp_rw [ContinuousLinearMapWOT.ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff,
    LinearMap.ext_iff]

Premises used: Function.Injective.eq_iff, LinearMap.ext_iff, separatingDual_iff_injective, Iff.mp, ContinuousLinearMapWOT.ext_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
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h :
  ∀ (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) : 𝕜₂)
⊢ ∀ (x : E) (x_1 : F →L[𝕜₂] 𝕜₂),
    Eq.{u_2 + 1} (α := 𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((A : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((B : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)

Tactic:
h
-- 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
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h :
  ∀ (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) : 𝕜₂)
⊢ ∀ (x : E) (x_1 : F →L[𝕜₂] 𝕜₂),
    Eq.{u_2 + 1} (α := 𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((A : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)
      ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((B : (a : E) → F) x) :
              (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
            (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
          x_1 :
        𝕜₂)

Tactic:
exact h
-- 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
S : Type u_5
inst_8 : DistribSMul S F
inst_9 : SMulCommClass 𝕜₂ S F
inst_10 : ContinuousConstSMul S F
c : S
f : E →SL[σ] F
⊢ ofCLM (c • f) = c • ofCLM 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
S : Type u_5
inst_8 : DistribSMul S F
inst_9 : SMulCommClass 𝕜₂ S F
inst_10 : ContinuousConstSMul S F
c : S
f : E →SWOT[σ] F
⊢ (c • f).toCLM = c • f.toCLM

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
S : Type u_5
inst_8 : DistribSMul S F
inst_9 : SMulCommClass 𝕜₂ S F
inst_10 : ContinuousConstSMul S F
f : E →SWOT[σ] F
c : S
x : E
⊢ (c • f : (a : E) → F) x = HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
inst : NormedField 𝕜₁
E : Type u_3
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜₁ E
S : Type u_5
inst_4 : CommSemiring S
inst_5 : Module S E
inst_6 : SMulCommClass 𝕜₁ S E
inst_7 : SMul S 𝕜₁
inst_8 : IsScalarTower S 𝕜₁ E
inst_9 : ContinuousConstSMul S E
inst_10 : IsTopologicalAddGroup E
c : S
⊢ Eq.{u_3 + 1} (α := E →L[𝕜₁] E) (toCLM ((algebraMap S (E →WOT[𝕜₁] E) : (a : S) → E →WOT[𝕜₁] E) c))
    ((algebraMap S (E →L[𝕜₁] E) : (a : S) → E →L[𝕜₁] E) c)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
inst : NormedField 𝕜₁
E : Type u_3
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜₁ E
S : Type u_5
inst_4 : CommSemiring S
inst_5 : Module S E
inst_6 : SMulCommClass 𝕜₁ S E
inst_7 : SMul S 𝕜₁
inst_8 : IsScalarTower S 𝕜₁ E
inst_9 : ContinuousConstSMul S E
inst_10 : IsTopologicalAddGroup E
c : S
⊢ Eq.{u_3 + 1} (α := E →WOT[𝕜₁] E) (ofCLM ((algebraMap S (E →L[𝕜₁] E) : (a : S) → E →L[𝕜₁] E) c))
    ((algebraMap S (E →WOT[𝕜₁] E) : (a : S) → E →WOT[𝕜₁] E) c)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_1
inst : NormedField 𝕜₁
E : Type u_3
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜₁ E
S : Type u_5
inst_4 : CommSemiring S
inst_5 : Module S E
inst_6 : SMulCommClass 𝕜₁ S E
inst_7 : SMul S 𝕜₁
inst_8 : IsScalarTower S 𝕜₁ E
inst_9 : ContinuousConstSMul S E
inst_10 : IsTopologicalAddGroup E
c : S
x : E
⊢ (((algebraMap S (E →WOT[𝕜₁] E) : (a : S) → E →WOT[𝕜₁] E) c : E →WOT[𝕜₁] E) : (a : E) → E) x = c • 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
⊢ Eq (α := E →SWOT[σ] F) (ofCLM 0) 0

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
f g : E →SL[σ] F
⊢ ofCLM (f + g) = ofCLM f + ofCLM g

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
f g : E →SL[σ] F
⊢ ofCLM (f - g) = ofCLM f - ofCLM g

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
f : E →SL[σ] F
⊢ ofCLM (-f) = -ofCLM f

Tactic:
rfl

Premises used: rfl
-- 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
f g : F →L[𝕜₂] F
⊢ ofCLM (f * g) = ofCLM f * ofCLM g

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq.{u_4 + 1} (α := F →WOT[𝕜₂] F) (ofCLM 1) 1

Tactic:
rfl

Premises used: rfl
-- 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
f : F →L[𝕜₂] F
n : ℕ
⊢ ofCLM (f ^ n) = ofCLM f ^ n

Tactic:
rfl

Premises used: rfl
-- 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 : ℕ
⊢ Eq.{u_4 + 1} (α := F →WOT[𝕜₂] F) (ofCLM (↑n : F →L[𝕜₂] F)) (↑n : F →WOT[𝕜₂] F)

Tactic:
rfl

Premises used: rfl
-- 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 : ℤ
⊢ Eq.{u_4 + 1} (α := F →WOT[𝕜₂] F) (ofCLM (↑n : F →L[𝕜₂] F)) (↑n : F →WOT[𝕜₂] 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
⊢ Eq (α := E →SL[σ] F) (toCLM 0) 0

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
f g : E →SWOT[σ] F
⊢ (f + g).toCLM = f.toCLM + g.toCLM

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
f g : E →SWOT[σ] F
⊢ (f - g).toCLM = f.toCLM - g.toCLM

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
f : E →SWOT[σ] F
⊢ (-f).toCLM = -f.toCLM

Tactic:
rfl

Premises used: rfl
-- 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
f g : F →WOT[𝕜₂] F
⊢ (f * g).toCLM = f.toCLM * g.toCLM

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq.{u_4 + 1} (α := F →L[𝕜₂] F) (toCLM 1) 1

Tactic:
rfl

Premises used: rfl
-- 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
f : F →WOT[𝕜₂] F
n : ℕ
⊢ (f ^ n).toCLM = f.toCLM ^ n

Tactic:
rfl

Premises used: rfl
-- 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 : ℕ
⊢ Eq.{u_4 + 1} (α := F →L[𝕜₂] F) (toCLM (↑n : F →WOT[𝕜₂] F)) (↑n : F →L[𝕜₂] F)

Tactic:
rfl

Premises used: rfl
-- 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 : ℤ
⊢ Eq.{u_4 + 1} (α := F →L[𝕜₂] F) (toCLM (↑n : F →WOT[𝕜₂] F)) (↑n : F →L[𝕜₂] 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
x : E
⊢ Eq.{u_4 + 1} (α := F) ((0 : (a : E) → F) x : F) (0 : 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
f g : E →SWOT[σ] F
x : E
⊢ (f + g : (a : E) → F) x = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (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
f g : E →SWOT[σ] F
x : E
⊢ (f - g : (a : E) → F) x = HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (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
f : E →SWOT[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F) ((-f : (a : E) → F) x : F) (-(f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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
f g : F →WOT[𝕜₂] F
x : F
⊢ Eq (α := F) ((f * g : (a : F) → F) x : F) ((f : (a : F) → F) ((g : (a : F) → F) x : F) : F)

Tactic:
rfl

Premises used: rfl
-- 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
x : F
⊢ (1 : (a : F) → F) x = x

Tactic:
rfl

Premises used: rfl
-- 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