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
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : NormedSpace ℝ 𝕜₂
inst_11 : Module ℝ (E →SWOT[σ] F)
inst_12 : IsScalarTower ℝ 𝕜₂ (E →SWOT[σ] F)
⊢ LocallyConvexSpace ℝ (E →SWOT[σ] F)

Tactic:
withSeminorms.toLocallyConvexSpace

Premises used: ContinuousLinearMapWOT.withSeminorms, WithSeminorms.toLocallyConvexSpace
-- 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 : ContinuousSMul 𝕜₁ E
⊢ Continuous[ContinuousLinearMap.topologicalSpace, instTopologicalSpace] ofCLM

Tactic:
ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y ↦
    y.cont.comp <| continuous_eval_const x

Premises used: Continuous.comp, ContinuousLinearMapWOT.continuous_of_dual_apply_continuous, ContinuousEvalConst.continuous_eval_const, ContinuousLinearMap.cont
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₂ : Type u_6
F : Type u_10
inst : NormedField 𝕜₂
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜₂ F
⊢ Eq (α := F →L[𝕜₂] F) (toCLM (ContinuousLinearMapWOT.id 𝕜₂ F)) (ContinuousLinearMap.id 𝕜₂ F)

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
g : F →SWOT[σ₂₃] G
f : E →SWOT[σ₁₂] F
x : E
⊢ Eq.{u_11 + 1} (α := G) ((g.comp f : (a : E) → G) x : G) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G)

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
g : F →SWOT[σ₂₃] G
f : E →SWOT[σ₁₂] F
⊢ (g.comp f).toCLM = g.toCLM ∘SL f.toCLM

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
E : Type u_9
F : Type u_10
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
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
⊢ comp (ContinuousLinearMapWOT.id 𝕜₂ F) f = f

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₂ : Type u_6
𝕜₃ : Type u_7
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₂
inst_1 : NormedField 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : Module 𝕜₂ F
inst_5 : AddCommGroup G
inst_6 : TopologicalSpace G
inst_7 : Module 𝕜₃ G
g : F →SWOT[σ₂₃] G
⊢ g.comp (ContinuousLinearMapWOT.id 𝕜₂ F) = g

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_5 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_6 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_7 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_8 : AddCommGroup E
inst_9 : TopologicalSpace E
inst_10 : Module 𝕜₁ E
inst_11 : AddCommGroup F
inst_12 : TopologicalSpace F
inst_13 : Module 𝕜₂ F
inst_14 : AddCommGroup G
inst_15 : TopologicalSpace G
inst_16 : Module 𝕜₃ G
inst_17 : AddCommGroup H
inst_18 : TopologicalSpace H
inst_19 : Module 𝕜₄ H
g₃₄ : G →SWOT[σ₃₄] H
g₂₃ : F →SWOT[σ₂₃] G
g₁₂ : E →SWOT[σ₁₂] F
⊢ (g₃₄.comp g₂₃).comp g₁₂ = g₃₄.comp (g₂₃.comp g₁₂)

Tactic:
simp only [comp, ContinuousLinearMap.comp_assoc]

Premises used: ContinuousLinearMapWOT.comp, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₂ : Type u_6
F : Type u_10
inst : NormedField 𝕜₂
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜₂ F
inst_4 : IsTopologicalAddGroup F
f g : F →WOT[𝕜₂] F
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: ContinuousLinearMapWOT.comp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (g : F →SWOT[σ₂₃] G) ↦ g.comp f

Tactic:
continuous_of_dual_apply_continuous fun _ _ ↦ continuous_dual_apply ..

Premises used: ContinuousLinearMap.toLinearMap, ContinuousLinearMapWOT.continuous_of_dual_apply_continuous, ContinuousLinearMapWOT.toCLM, DFunLike.coe, ContinuousLinearMapWOT.continuous_dual_apply
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (f : E →SWOT[σ₁₂] F) ↦ g.comp f

Tactic:
continuous_of_dual_apply_continuous fun x z ↦ ?_

Premises used: ContinuousLinearMapWOT.continuous_of_dual_apply_continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
refine :
  ∀ (x : E) (z : StrongDual 𝕜₃ G),
    Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
      (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (f : E →SWOT[σ₁₂] F) ↦ g.comp f

Tactic:
refine continuous_of_dual_apply_continuous fun x z ↦ ?_

Premises used: ContinuousLinearMapWOT.continuous_of_dual_apply_continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
⊢ Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)

Tactic:
have σ_bij : Function.Bijective σ₂₃ := ⟨σ₂₃.injective, RingHomSurjective.is_surjective⟩
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
h : ∀ (a : E →SWOT[σ₁₂] F), ((z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G) : 𝕜₃)
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)

Tactic:
enter [1, a]
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
a : E →SWOT[σ₁₂] F
h :
  ((σ_li : (a : 𝕜₂) → 𝕜₃)
      ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
        𝕜₂) :
    𝕜₃)
| ((z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G) : 𝕜₃)

Tactic:
rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply, ContinuousLinearMapWOT.comp_apply, ContinuousLinearMapWOT.toCLM_apply, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
h :
  ∀ (a : E →SWOT[σ₁₂] F),
    ((σ_li : (a : 𝕜₂) → 𝕜₃)
        ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
          𝕜₂) :
      𝕜₃)
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)

Tactic:
enter [1, a]; rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply, ContinuousLinearMapWOT.comp_apply, ContinuousLinearMapWOT.toCLM_apply, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
conv :
  Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li : (a : 𝕜₂) → 𝕜₃)
      ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
        𝕜₂)
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)

Tactic:
conv => enter [1, a]; rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply, ContinuousLinearMapWOT.comp_apply, ContinuousLinearMapWOT.toCLM_apply, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
apply :
  Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃)
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li : (a : 𝕜₂) → 𝕜₃)
      ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
        𝕜₂)

Tactic:
apply σ_li.continuous.comp

Premises used: Continuous.comp, LinearIsometryEquiv.continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃)

Tactic:
continuous_dual_apply x <| σ_li.symm.toLinearIsometry.toContinuousLinearMap.comp <|
    z.comp g.toCLM

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, ContinuousLinearMapWOT.toCLM, ContinuousLinearMapWOT.continuous_dual_apply, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃)

Tactic:
exact continuous_dual_apply x <| σ_li.symm.toLinearIsometry.toContinuousLinearMap.comp <|
    z.comp g.toCLM

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, ContinuousLinearMapWOT.toCLM, ContinuousLinearMapWOT.continuous_dual_apply, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (x y : F →SWOT[σ₂₃] G), (x + y).comp f = x.comp f + y.comp f

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp