awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this_3 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f
have rw : Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
  (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
    (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
      (DFunLike.coe (β := fun (a : E) ↦ G)))
    fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f)
Tactic: rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
⊢ ContinuousLinearMap.pi (φ := F) (x + x_1) = ContinuousLinearMap.pi (φ := F) x + ContinuousLinearMap.pi (φ := F) x_1
have h : ∀ (x_2 : E) (x_3 : ι),
  Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x + x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
    ((ContinuousLinearMap.pi (φ := F) x + ContinuousLinearMap.pi (φ := F) x_1 : (a : E) → (i : ι) → F i) x_2 x_3 :
      F x_3)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 : 𝕜
x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
⊢ ContinuousLinearMap.pi (φ := F) (x • x_1) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (ContinuousLinearMap.pi (φ := F) x_1)
have h : ∀ (x_2 : E) (x_3 : ι),
  Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x • x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (ContinuousLinearMap.pi (φ := F) x_1) :
          (a : E) → (i : ι) → F i)
        x_2 x_3 :
      F x_3)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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) 𝔖
⊢ (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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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) 𝔖
⊢ (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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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, 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
have 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)
Tactic: rw [UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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, 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)
have 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))
Tactic: rw [UniformOnFun.uniformEquivPiComm _ _ |>.isUniformEmbedding.isEmbedding.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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))
have 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
Tactic: refine continuous_pi fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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[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
have 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
Tactic: apply continuous_pi (A := fun i ↦ E →Lᵤ[𝕜, 𝔖] F i) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective (α := E) (β := F →ₗ[𝕜] 𝕜) (⇑B : (a : E) → F →ₗ[𝕜] 𝕜)
⊢ Tendsto f l (𝓝 x) ↔
    ∀ (y : F),
      Tendsto.{u_1, u_2} (β := 𝕜) (fun (i : α) ↦ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (f i) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
        l (𝓝 ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) : Filter 𝕜)
have rw : Tendsto (β := (y : F) → 𝕜)
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ f) l
    (𝓝 fun (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ↔
  Tendsto (β := (i : F) → 𝕜) (fun (i : α) ↦ (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) (f i) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)) l
    (𝓝 (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜))
Tactic: rw [← tendsto_pi_nhds, (isEmbedding hB).tendsto_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ ContinuousAdd.{u_4} (WeakBilin B)
have refine : Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
  ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
    fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
Tactic: refine ⟨continuous_induced_rng.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
have cast : HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) =
  (fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
    fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2
Tactic: refine
    cast (congr_arg _ ?_)
      (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) =
    (fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2
have h : ∀ (x : WeakBilin B × WeakBilin B) (x_1 : F),
  HAdd.hAdd (α := WeakBilin B × WeakBilin B → (y : F) → 𝕜) (β := WeakBilin B × WeakBilin B → (y : F) → 𝕜)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.fst)
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x x_1 =
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (p : WeakBilin B × WeakBilin B) ↦ p.1 + p.2)
      x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul.{u_2, u_4} 𝕜 (WeakBilin B)
have refine : Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
  ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
    fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
Tactic: refine ⟨continuous_induced_rng.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
have refine : Eq (α := Prod.{u_2, u_4} 𝕜 (WeakBilin B) → (y : F) → 𝕜)
  (fun (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦
    HSMul.hSMul (β := (y : F) → 𝕜) x.1
      (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x))
  ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
    fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
Tactic: refine cast (congr_arg _ ?_) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
⊢ Eq (α := Prod.{u_2, u_4} 𝕜 (WeakBilin B) → (y : F) → 𝕜)
    (fun (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦
      HSMul.hSMul (β := (y : F) → 𝕜) x.1
        (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x))
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
have h : ∀ (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) (x_1 : F),
  HSMul.hSMul (β := (y : F) → 𝕜) x.1
      (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x)
      x_1 =
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
      x x_1
Tactic: ext