awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
h :
  ∀ (x_1 : ι) (x_2 : E),
    Eq.{u_9 + 1} (α := F x_1)
      ((((fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
                  (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
                    ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
                ((fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
                    ContinuousLinearMap.pi (φ := F) F_2)
                  x)
                x_1 :
              ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F x_1)) :
            (a : E) → F x_1)
          x_2 :
        F x_1)
      ((x x_1 : (a : E) → F x_1) x_2 : F x_1)
⊢ (fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
          ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
      ((fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
          ContinuousLinearMap.pi (φ := F) F_2)
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
x_1 : ι
x_2 : E
⊢ Eq.{u_9 + 1} (α := F x_1)
    ((((fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
                  ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
              ((fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
                  ContinuousLinearMap.pi (φ := F) F_2)
                x)
              x_1 :
            ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F x_1)) :
          (a : E) → F x_1)
        x_2 :
      F x_1)
    ((x x_1 : (a : E) → F x_1) x_2 : F x_1)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖
h :
  ∀ (x_1 : E) (x_2 : ι),
    Eq.{u_9 + 1} (α := F x_2)
      (((fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
                ContinuousLinearMap.pi (φ := F) F_2)
              ((fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
                  (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
                    ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
                x) :
            (a : E) → (i : ι) → F i)
          x_1 x_2 :
        F x_2)
      ((x : (a : E) → (i : ι) → F i) x_1 x_2 : F x_2)
⊢ (fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2)
      ((fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
            ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖
x_1 : E
x_2 : ι
⊢ Eq.{u_9 + 1} (α := F x_2)
    (((fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
              ContinuousLinearMap.pi (φ := F) F_2)
            ((fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f :
                  ContinuousLinearMap.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) E (F i)))
              x) :
          (a : E) → (i : ι) → F i)
        x_1 x_2 :
      F x_2)
    ((x : (a : E) → (i : ι) → F i) x_1 x_2 : F x_2)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
rw :
  Continuous[Pi.topologicalSpace, UniformOnFun.topologicalSpace E ((i : ι) → F i) 𝔖]
    (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
      (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
        (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
      fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
      ContinuousLinearMap.pi (φ := F) F_2)
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖]
    fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
    ContinuousLinearMap.pi (φ := F) F_2

Tactic:
rw [UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous_iff]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
rw :
  Continuous[Pi.topologicalSpace, (Pi.uniformSpace fun (i : ι) ↦ E →ᵤ[𝔖] F i).toTopologicalSpace]
    (comp (β := E →ᵤ[𝔖] (i : ι) → F i)
      (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
      (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
        (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
          (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
        fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2))
⊢ Continuous[Pi.topologicalSpace, UniformOnFun.topologicalSpace E ((i : ι) → F i) 𝔖]
    (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
      (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
        (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
      fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
      ContinuousLinearMap.pi (φ := F) F_2)

Tactic:
rw [UniformOnFun.uniformEquivPiComm _ _ |>.isUniformEmbedding.isEmbedding.continuous_iff]

Premises used: IsUniformEmbedding.isEmbedding, UniformEquiv.isUniformEmbedding, UniformOnFun.uniformEquivPiComm, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
⊢ Continuous[Pi.topologicalSpace, (Pi.uniformSpace fun (i : ι) ↦ E →ᵤ[𝔖] F i).toTopologicalSpace]
    (comp (β := E →ᵤ[𝔖] (i : ι) → F i)
      (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
      (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
        (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
          (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
        fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2))

Tactic:
continuous_pi fun i ↦ ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
refine :
  ∀ (i : ι),
    Continuous[Pi.topologicalSpace, ((fun (i : ι) ↦ UniformOnFun.uniformSpace E (F i) 𝔖) i).toTopologicalSpace]
      fun (a : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
      comp (β := E →ᵤ[𝔖] (i : ι) → F i)
        (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
        (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
          (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
            (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
          fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
          ContinuousLinearMap.pi (φ := F) F_2)
        a i
⊢ Continuous[Pi.topologicalSpace, (Pi.uniformSpace fun (i : ι) ↦ E →ᵤ[𝔖] F i).toTopologicalSpace]
    (comp (β := E →ᵤ[𝔖] (i : ι) → F i)
      (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
      (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
        (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
          (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
        fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2))

Tactic:
refine continuous_pi fun i ↦ ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
i : ι
⊢ Continuous[Pi.topologicalSpace, ((fun (i : ι) ↦ UniformOnFun.uniformSpace E (F i) 𝔖) i).toTopologicalSpace]
    fun (a : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
    comp (β := E →ᵤ[𝔖] (i : ι) → F i)
      (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
      (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
        (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
          (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
        fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2)
      a i

Tactic:
UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous.comp (continuous_apply i)

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, continuous_apply, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
i : ι
⊢ Continuous[Pi.topologicalSpace, ((fun (i : ι) ↦ UniformOnFun.uniformSpace E (F i) 𝔖) i).toTopologicalSpace]
    fun (a : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
    comp (β := E →ᵤ[𝔖] (i : ι) → F i)
      (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) : (a : E →ᵤ[𝔖] (i : ι) → F i) → (i : ι) → E →ᵤ[𝔖] F i)
      (comp (β := UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖)
        (comp (β := E → (i : ι) → F i) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → (i : ι) → F i) → E →ᵤ[𝔖] (i : ι) → F i)
          (DFunLike.coe (β := fun (a : E) ↦ (i : ι) → F i)))
        fun (F_2 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖) ↦
        ContinuousLinearMap.pi (φ := F) F_2)
      a i

Tactic:
exact UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous.comp (continuous_apply i)

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
apply :
  ∀ (i : ι),
    Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, instTopologicalSpace (RingHom.id 𝕜) (F i) 𝔖]
      fun (a : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) a
⊢ Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, Pi.topologicalSpace]
    fun (f : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (i : ι) ↦
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) f

Tactic:
apply continuous_pi (A := fun i ↦ E →Lᵤ[𝕜, 𝔖] F i) fun i ↦ ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
i : ι
⊢ Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, instTopologicalSpace (RingHom.id 𝕜) (F i) 𝔖]
    fun (a : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) ↦
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) a

Tactic:
(ContinuousLinearMap.proj i : (Π j, F j) →L[𝕜] F i).postcompUniformConvergenceCLM 𝔖
        |>.continuous

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.continuous, ContinuousLinearMap.proj, ContinuousLinearMap.postcompUniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
i : ι
⊢ Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, instTopologicalSpace (RingHom.id 𝕜) (F i) 𝔖]
    fun (a : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) ↦
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := F) i) a

Tactic:
exact (ContinuousLinearMap.proj i : (Π j, F j) →L[𝕜] F i).postcompUniformConvergenceCLM 𝔖
        |>.continuous

Premises used: ContinuousLinearMap.continuous, ContinuousLinearMap.proj, ContinuousLinearMap.postcompUniformConvergenceCLM