diff --git a/Mathlib.lean b/Mathlib.lean
index 7ba04a7c6a7f7..4bcd6991efd04 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4613,6 +4613,7 @@ import Mathlib.Topology.Connected.PathConnected
 import Mathlib.Topology.Connected.Separation
 import Mathlib.Topology.Connected.TotallyDisconnected
 import Mathlib.Topology.Constructions
+import Mathlib.Topology.ContinuousEvalConst
 import Mathlib.Topology.ContinuousMap.Algebra
 import Mathlib.Topology.ContinuousMap.Basic
 import Mathlib.Topology.ContinuousMap.Bounded
@@ -4620,6 +4621,7 @@ import Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
 import Mathlib.Topology.ContinuousMap.CocompactMap
 import Mathlib.Topology.ContinuousMap.Compact
 import Mathlib.Topology.ContinuousMap.CompactlySupported
+import Mathlib.Topology.ContinuousMap.ContinuousEval
 import Mathlib.Topology.ContinuousMap.ContinuousMapZero
 import Mathlib.Topology.ContinuousMap.Defs
 import Mathlib.Topology.ContinuousMap.Ideals
diff --git a/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean b/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
index 52173af64e2c0..51f74ea999dc8 100644
--- a/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
+++ b/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
@@ -33,14 +33,9 @@ open Filter in
 lemma tendsto_iff_forall_inner_apply_tendsto [CompleteSpace F] {α : Type*} {l : Filter α}
     {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} :
     Tendsto f l (𝓝 A) ↔ ∀ x y, Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜) := by
-  simp only [← InnerProductSpace.toDual_apply]
-  refine ⟨fun h x y => ?_, fun h => ?_⟩
-  · exact (tendsto_iff_forall_dual_apply_tendsto.mp h) _ _
-  · have h' : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F),
-        Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))) := by
-      intro x y
-      convert h x ((InnerProductSpace.toDual 𝕜 F).symm y) <;> simp
-    exact tendsto_iff_forall_dual_apply_tendsto.mpr h'
+  simp_rw [tendsto_iff_forall_dual_apply_tendsto, ← InnerProductSpace.toDual_apply]
+  exact .symm <| forall_congr' fun _ ↦
+    Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl
 
 lemma le_nhds_iff_forall_inner_apply_le_nhds [CompleteSpace F] {l : Filter (E →WOT[𝕜] F)}
     {A : E →WOT[𝕜] F} : l ≤ 𝓝 A ↔ ∀ x y, l.map (fun T => ⟪y, T x⟫_𝕜) ≤ 𝓝 (⟪y, A x⟫_𝕜) :=
diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
index b4165a1a77053..0962d64ab3617 100644
--- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
+++ b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -877,13 +877,22 @@ protected def SeminormFamily.sigma {κ : ι → Type*} (p : (i : ι) → Seminor
 
 theorem withSeminorms_iInf {κ : ι → Type*} [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)]
     {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E}
-    [∀ i, @TopologicalAddGroup E (t i) _] (hp : ∀ i, WithSeminorms (topology := t i) (p i)) :
+    (hp : ∀ i, WithSeminorms (topology := t i) (p i)) :
     WithSeminorms (topology := ⨅ i, t i) (SeminormFamily.sigma p) := by
-  have : @TopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf (fun i ↦ inferInstance)
+  have : ∀ i, @TopologicalAddGroup E (t i) _ :=
+    fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ _ (t i) _ (hp i)
+  have : @TopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance
   simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢
   rw [iInf_sigma]
   exact iInf_congr hp
 
+theorem withSeminorms_pi {κ : ι → Type*} {E : ι → Type*}
+    [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
+    [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)}
+    (hp : ∀ i, WithSeminorms (p i)) :
+    WithSeminorms (SeminormFamily.sigma (fun i ↦ (p i).comp (LinearMap.proj i))) :=
+  withSeminorms_iInf fun i ↦ (LinearMap.proj i).withSeminorms_induced (hp i)
+
 end TopologicalConstructions
 
 section TopologicalProperties
diff --git a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean
index 45dfa1892cbcc..574b200a3371e 100644
--- a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean
+++ b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis
 -/
 
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
-import Mathlib.Analysis.Normed.Module.Dual
+import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
 
 /-!
 # The weak operator topology
@@ -57,14 +57,15 @@ def ContinuousLinearMapWOT (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜
   E →L[𝕜] F
 
 @[inherit_doc]
-notation:25 E " →WOT[" 𝕜 "]" F => ContinuousLinearMapWOT 𝕜 E F
+notation:25 E " →WOT[" 𝕜 "] " F => ContinuousLinearMapWOT 𝕜 E F
 
 namespace ContinuousLinearMapWOT
 
-variable {𝕜 : Type*} {E : Type*} {F : Type*} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E]
-  [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {𝕜 : Type*} {E : Type*} {F : Type*} [NormedField 𝕜]
+  [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E]
+  [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F]
 
-local postfix:max "⋆" => NormedSpace.Dual 𝕜
+local notation X "⋆" => X →L[𝕜] 𝕜
 
 /-!
 ### Basic properties common with `E →L[𝕜] F`
@@ -75,18 +76,21 @@ the module structure, `FunLike`, etc.
 section Basic
 
 unseal ContinuousLinearMapWOT in
-instance instAddCommGroup : AddCommGroup (E →WOT[𝕜] F) :=
+instance instAddCommGroup [TopologicalAddGroup F] : AddCommGroup (E →WOT[𝕜] F) :=
   inferInstanceAs <| AddCommGroup (E →L[𝕜] F)
 
 unseal ContinuousLinearMapWOT in
-instance instModule : Module 𝕜 (E →WOT[𝕜] F) := inferInstanceAs <| Module 𝕜 (E →L[𝕜] F)
+instance instModule [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : Module 𝕜 (E →WOT[𝕜] F) :=
+  inferInstanceAs <| Module 𝕜 (E →L[𝕜] F)
 
-variable (𝕜) (E) (F)
+variable (𝕜) (E) (F) [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
 
 unseal ContinuousLinearMapWOT in
 /-- The linear equivalence that sends a continuous linear map to the type copy endowed with the
 weak operator topology. -/
-def _root_.ContinuousLinearMap.toWOT : (E →L[𝕜] F) ≃ₗ[𝕜] (E →WOT[𝕜] F) := LinearEquiv.refl 𝕜 _
+def _root_.ContinuousLinearMap.toWOT :
+    (E →L[𝕜] F) ≃ₗ[𝕜] (E →WOT[𝕜] F) :=
+  LinearEquiv.refl 𝕜 _
 
 variable {𝕜} {E} {F}
 
@@ -112,11 +116,10 @@ lemma ext_iff {A B : E →WOT[𝕜] F} : A = B ↔ ∀ x, A x = B x := Continuou
 -- version with an inner product (`ContinuousLinearMapWOT.ext_inner`) takes precedence
 -- in the case of Hilbert spaces.
 @[ext 900]
-lemma ext_dual {A B : E →WOT[𝕜] F} (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B := by
-  rw [ext_iff]
-  intro x
-  specialize h x
-  rwa [← NormedSpace.eq_iff_forall_dual_eq 𝕜] at h
+lemma ext_dual [H : SeparatingDual 𝕜 F] {A B : E →WOT[𝕜] F}
+    (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B := by
+  simp_rw [ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff, LinearMap.ext_iff]
+  exact h
 
 @[simp] lemma zero_apply (x : E) : (0 : E →WOT[𝕜] F) x = 0 := by simp only [DFunLike.coe]; rfl
 
@@ -146,6 +149,8 @@ of this topology. In particular, we show that it is a topological vector space.
 -/
 section Topology
 
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
+
 variable (𝕜) (E) (F) in
 /-- The function that induces the topology on `E →WOT[𝕜] F`, namely the function that takes
 an `A` and maps it to `fun ⟨x, y⟩ => y (A x)` in `E × F⋆ → 𝕜`, bundled as a linear map to make
@@ -155,6 +160,11 @@ def inducingFn : (E →WOT[𝕜] F) →ₗ[𝕜] (E × F⋆ → 𝕜) where
   map_add' := fun x y => by ext; simp
   map_smul' := fun x y => by ext; simp
 
+@[simp]
+lemma inducingFn_apply {f : E →WOT[𝕜] F} {x : E} {y : F⋆} :
+    inducingFn 𝕜 E F f (x, y) = y (f x) :=
+  rfl
+
 /-- The weak operator topology is the coarsest topology such that `fun A => y (A x)` is
 continuous for all `x, y`. -/
 instance instTopologicalSpace : TopologicalSpace (E →WOT[𝕜] F) :=
@@ -172,7 +182,9 @@ lemma continuous_of_dual_apply_continuous {α : Type*} [TopologicalSpace α] {g
     (h : ∀ x (y : F⋆), Continuous fun a => y (g a x)) : Continuous g :=
   continuous_induced_rng.2 (continuous_pi_iff.mpr fun p => h p.1 p.2)
 
-lemma embedding_inducingFn : Embedding (inducingFn 𝕜 E F) := by
+lemma inducing_inducingFn : Inducing (inducingFn 𝕜 E F) := ⟨rfl⟩
+
+lemma embedding_inducingFn [SeparatingDual 𝕜 F] : Embedding (inducingFn 𝕜 E F) := by
   refine Function.Injective.embedding_induced fun A B hAB => ?_
   rw [ContinuousLinearMapWOT.ext_dual_iff]
   simpa [Function.funext_iff] using hAB
@@ -183,17 +195,13 @@ open Filter in
 lemma tendsto_iff_forall_dual_apply_tendsto {α : Type*} {l : Filter α} {f : α → E →WOT[𝕜] F}
     {A : E →WOT[𝕜] F} :
     Tendsto f l (𝓝 A) ↔ ∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))) := by
-  have hmain : (∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))))
-      ↔ ∀ (p : E × F⋆), Tendsto (fun a => p.2 (f a p.1)) l (𝓝 (p.2 (A p.1))) :=
-    ⟨fun h p => h p.1 p.2, fun h x y => h ⟨x, y⟩⟩
-  rw [hmain, ← tendsto_pi_nhds, Embedding.tendsto_nhds_iff embedding_inducingFn]
-  rfl
+  simp [inducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]
 
 lemma le_nhds_iff_forall_dual_apply_le_nhds {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} :
     l ≤ 𝓝 A ↔ ∀ x (y : F⋆), l.map (fun T => y (T x)) ≤ 𝓝 (y (A x)) :=
   tendsto_iff_forall_dual_apply_tendsto (f := id)
 
-instance instT3Space : T3Space (E →WOT[𝕜] F) := embedding_inducingFn.t3Space
+instance instT3Space [SeparatingDual 𝕜 F] : T3Space (E →WOT[𝕜] F) := embedding_inducingFn.t3Space
 
 instance instContinuousAdd : ContinuousAdd (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F)
 instance instContinuousNeg : ContinuousNeg (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F)
@@ -210,6 +218,8 @@ end Topology
 /-! ### The WOT is induced by a family of seminorms -/
 section Seminorms
 
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
+
 /-- The family of seminorms that induce the weak operator topology, namely `‖y (A x)‖` for
 all `x` and `y`. -/
 def seminorm (x : E) (y : F⋆) : Seminorm 𝕜 (E →WOT[𝕜] F) where
@@ -225,56 +235,38 @@ all `x` and `y`. -/
 def seminormFamily : SeminormFamily 𝕜 (E →WOT[𝕜] F) (E × F⋆) :=
   fun ⟨x, y⟩ => seminorm x y
 
-lemma hasBasis_seminorms : (𝓝 (0 : E →WOT[𝕜] F)).HasBasis (seminormFamily 𝕜 E F).basisSets id := by
-  let p := seminormFamily 𝕜 E F
-  rw [nhds_induced, nhds_pi]
-  simp only [map_zero, Pi.zero_apply]
-  have h := Filter.hasBasis_pi (fun _ : (E × F⋆) ↦ Metric.nhds_basis_ball (x := 0)) |>.comap
-    (inducingFn 𝕜 E F)
-  refine h.to_hasBasis' ?_ ?_
-  · rintro ⟨s, U₂⟩ ⟨hs, hU₂⟩
-    lift s to Finset (E × F⋆) using hs
-    by_cases hU₃ : s.Nonempty
-    · refine ⟨(s.sup p).ball 0 <| s.inf' hU₃ U₂, p.basisSets_mem _ <| (Finset.lt_inf'_iff _).2 hU₂,
-        fun x hx y hy => ?_⟩
-      simp only [Set.mem_preimage, Set.mem_pi, mem_ball_zero_iff]
-      rw [id, Seminorm.mem_ball_zero] at hx
-      have hp : p y ≤ s.sup p := Finset.le_sup hy
-      refine lt_of_le_of_lt (hp x) (lt_of_lt_of_le hx ?_)
-      exact Finset.inf'_le _ hy
-    · rw [Finset.not_nonempty_iff_eq_empty.mp hU₃]
-      exact ⟨(p 0).ball 0 1, p.basisSets_singleton_mem 0 one_pos, by simp⟩
-  · suffices ∀ U ∈ p.basisSets, U ∈ 𝓝 (0 : E →WOT[𝕜] F) by simpa [nhds_induced, nhds_pi]
-    exact p.basisSets_mem_nhds fun ⟨x, y⟩ ↦ continuous_dual_apply x y |>.norm
-
 lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E F) :=
-  SeminormFamily.withSeminorms_of_hasBasis _ hasBasis_seminorms
+  let e : E × F⋆ ≃ (Σ _ : E × F⋆, Fin 1) := .symm <| .sigmaUnique _ _
+  have : Nonempty (Σ _ : E × F⋆, Fin 1) := e.symm.nonempty
+  inducing_inducingFn.withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜)
+    |>.congr_equiv e
+
+lemma hasBasis_seminorms : (𝓝 (0 : E →WOT[𝕜] F)).HasBasis (seminormFamily 𝕜 E F).basisSets id :=
+  withSeminorms.hasBasis
 
-instance instLocallyConvexSpace [Module ℝ (E →WOT[𝕜] F)] [IsScalarTower ℝ 𝕜 (E →WOT[𝕜] F)] :
+instance instLocallyConvexSpace [NormedSpace ℝ 𝕜] [Module ℝ (E →WOT[𝕜] F)]
+    [IsScalarTower ℝ 𝕜 (E →WOT[𝕜] F)] :
     LocallyConvexSpace ℝ (E →WOT[𝕜] F) :=
   withSeminorms.toLocallyConvexSpace
 
 end Seminorms
 
-end ContinuousLinearMapWOT
-
-section NormedSpace
+section toWOT_continuous
 
-variable {𝕜 : Type*} {E : Type*} {F : Type*} [RCLike 𝕜] [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E]
 
-/-- The weak operator topology is coarser than the norm topology, i.e. the inclusion map is
-continuous. -/
+/-- The weak operator topology is coarser than the bounded convergence topology, i.e. the inclusion
+map is continuous. -/
 @[continuity, fun_prop]
 lemma ContinuousLinearMap.continuous_toWOT :
-    Continuous (ContinuousLinearMap.toWOT 𝕜 E F) := by
-  refine ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y => ?_
-  simp_rw [ContinuousLinearMap.toWOT_apply]
-  change Continuous fun a => y <| (ContinuousLinearMap.id 𝕜 (E →L[𝕜] F)).flip x a
-  fun_prop
+    Continuous (ContinuousLinearMap.toWOT 𝕜 E F) :=
+  ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y ↦
+    y.cont.comp <| continuous_eval_const x
 
 /-- The inclusion map from `E →[𝕜] F` to `E →WOT[𝕜] F`, bundled as a continuous linear map. -/
 def ContinuousLinearMap.toWOTCLM : (E →L[𝕜] F) →L[𝕜] (E →WOT[𝕜] F) :=
   ⟨LinearEquiv.toLinearMap (ContinuousLinearMap.toWOT 𝕜 E F), ContinuousLinearMap.continuous_toWOT⟩
 
-end NormedSpace
+end toWOT_continuous
+
+end ContinuousLinearMapWOT
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
index 4b87da345fe31..c4dd9fd8a30d5 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -80,16 +80,19 @@ variable {𝕜 ι : Type*} {E : ι → Type*} {F : Type*}
     [NormedField 𝕜] [Finite ι] [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
     [TopologicalSpace F] [AddCommGroup F] [TopologicalAddGroup F] [Module 𝕜 F]
 
-/-- Applying a multilinear map to a vector is continuous in both coordinates. -/
-theorem ContinuousMultilinearMap.continuous_eval :
-    Continuous fun p : ContinuousMultilinearMap 𝕜 E F × ∀ i, E i => p.1 p.2 := by
-  cases nonempty_fintype ι
-  let _ := TopologicalAddGroup.toUniformSpace F
-  have := comm_topologicalAddGroup_is_uniform (G := F)
-  refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
-    (embedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt
-  exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
-    ball_mem_nhds _ one_pos⟩
+instance ContinuousMultilinearMap.instContinuousEval :
+    ContinuousEval (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
+  continuous_eval := by
+    cases nonempty_fintype ι
+    let _ := TopologicalAddGroup.toUniformSpace F
+    have := comm_topologicalAddGroup_is_uniform (G := F)
+    refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
+      (embedding_toUniformOnFun.continuous.prod_map continuous_id) fun (f, x) ↦ f.cont.continuousAt
+    exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
+      ball_mem_nhds _ one_pos⟩
+
+@[deprecated (since := "2024-10-05")]
+protected alias ContinuousMultilinearMap.continuous_eval := continuous_eval
 
 namespace ContinuousLinearMap
 
@@ -97,8 +100,8 @@ variable {G : Type*} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [Cont
   (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
 
 lemma continuous_uncurry_of_multilinear :
-    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) :=
-  ContinuousMultilinearMap.continuous_eval.comp <| .prodMap (map_continuous f) continuous_id
+    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) := by
+  fun_prop
 
 lemma continuousOn_uncurry_of_multilinear {s} :
     ContinuousOn (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s :=
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean
index 783b55750d8fb..602f64ecca7c2 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean
+++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean
@@ -48,7 +48,7 @@ def ofMemClosureImageCoeBounded (f : E' → F) {s : Set (E' →SL[σ₁₂] F)}
     rcases isBounded_iff_forall_norm_le.1 hs with ⟨C, hC⟩
     -- Then `‖g x‖ ≤ C * ‖x‖` for all `g ∈ s`, `x : E`, hence `‖f x‖ ≤ C * ‖x‖` for all `x`.
     have : ∀ x, IsClosed { g : E' → F | ‖g x‖ ≤ C * ‖x‖ } := fun x =>
-      isClosed_Iic.preimage (@continuous_apply E' (fun _ => F) _ x).norm
+      isClosed_Iic.preimage (@_root_.continuous_apply E' (fun _ => F) _ x).norm
     refine ⟨C, fun x => (this x).closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf⟩
     exact g.le_of_opNorm_le (hC _ hg) _
 
@@ -153,7 +153,7 @@ theorem is_weak_closed_closedBall (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f :
   have hr : 0 ≤ r := nonempty_closedBall.1 (closure_nonempty_iff.1 ⟨_, hf⟩).of_image
   refine mem_closedBall_iff_norm.2 (opNorm_le_bound _ hr fun x => ?_)
   have : IsClosed { g : E' → F | ‖g x - f₀ x‖ ≤ r * ‖x‖ } :=
-    isClosed_Iic.preimage ((@continuous_apply E' (fun _ => F) _ x).sub continuous_const).norm
+    isClosed_Iic.preimage ((@_root_.continuous_apply E' (fun _ => F) _ x).sub continuous_const).norm
   refine this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf
   exact (g - f₀).le_of_opNorm_le (mem_closedBall_iff_norm.1 hg) _
 
diff --git a/Mathlib/Analysis/ODE/PicardLindelof.lean b/Mathlib/Analysis/ODE/PicardLindelof.lean
index 9c46abf777613..e4c1e95974594 100644
--- a/Mathlib/Analysis/ODE/PicardLindelof.lean
+++ b/Mathlib/Analysis/ODE/PicardLindelof.lean
@@ -223,10 +223,10 @@ instance [CompleteSpace E] : CompleteSpace v.FunSpace := by
   refine (completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap).2
       (IsClosed.isComplete ?_)
   rw [range_toContinuousMap, setOf_and]
-  refine (isClosed_eq (ContinuousMap.continuous_eval_const _) continuous_const).inter ?_
+  refine (isClosed_eq (continuous_eval_const _) continuous_const).inter ?_
   have : IsClosed {f : Icc v.tMin v.tMax → E | LipschitzWith v.C f} :=
     isClosed_setOf_lipschitzWith v.C
-  exact this.preimage ContinuousMap.continuous_coe
+  exact this.preimage continuous_coeFun
 
 theorem intervalIntegrable_vComp (t₁ t₂ : ℝ) : IntervalIntegrable f.vComp volume t₁ t₂ :=
   f.continuous_vComp.intervalIntegrable _ _
diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
index a753c9397ac13..1aeab011ea67d 100644
--- a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
+++ b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
@@ -244,6 +244,15 @@ theorem embedding_toContinuousMap :
     Embedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
   ⟨inducing_toContinuousMap A B, toContinuousMap_injective⟩
 
+@[to_additive]
+instance instContinuousEvalConst : ContinuousEvalConst (ContinuousMonoidHom A B) A B :=
+  .of_continuous_forget (inducing_toContinuousMap A B).continuous
+
+@[to_additive]
+instance instContinuousEval [LocallyCompactPair A B] :
+    ContinuousEval (ContinuousMonoidHom A B) A B :=
+  .of_continuous_forget (inducing_toContinuousMap A B).continuous
+
 @[to_additive]
 lemma range_toContinuousMap :
     Set.range (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) =
@@ -258,10 +267,10 @@ theorem closedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] :
   toEmbedding := embedding_toContinuousMap A B
   isClosed_range := by
     simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]
-    refine .inter (isClosed_singleton.preimage (ContinuousMap.continuous_eval_const 1)) <|
+    refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
       isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_
-    exact isClosed_eq (ContinuousMap.continuous_eval_const (x * y)) <|
-      .mul (ContinuousMap.continuous_eval_const x) (ContinuousMap.continuous_eval_const y)
+    exact isClosed_eq (continuous_eval_const (x * y)) <|
+      .mul (continuous_eval_const x) (continuous_eval_const y)
 
 variable {A B C D E}
 
diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
index 32efbbd5a39c7..fa89046524524 100644
--- a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
+++ b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
@@ -36,7 +36,7 @@ lemma isClosed_range_toContinuousMultilinearMap [ContinuousSMul 𝕜 E] [T2Space
       ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F)) := by
   simp only [range_toContinuousMultilinearMap, setOf_forall]
   repeat refine isClosed_iInter fun _ ↦ ?_
-  exact isClosed_singleton.preimage (ContinuousMultilinearMap.continuous_eval_const _)
+  exact isClosed_singleton.preimage (continuous_eval_const _)
 
 end IsClosedRange
 
@@ -119,6 +119,11 @@ end UniformAddGroup
 
 variable [TopologicalSpace F] [TopologicalAddGroup F]
 
+instance instTopologicalAddGroup : TopologicalAddGroup (E [⋀^ι]→L[𝕜] F) :=
+  letI := TopologicalAddGroup.toUniformSpace F
+  haveI := comm_topologicalAddGroup_is_uniform (G := F)
+  inferInstance
+
 lemma embedding_toContinuousMultilinearMap :
     Embedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) :=
   letI := TopologicalAddGroup.toUniformSpace F
@@ -159,21 +164,19 @@ lemma closedEmbedding_toContinuousMultilinearMap [T2Space F] :
       (E [⋀^ι]→L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F) :=
   ⟨embedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩
 
-@[continuity, fun_prop]
-theorem continuous_eval_const (x : ι → E) :
-    Continuous fun p : E [⋀^ι]→L[𝕜] F ↦ p x :=
-  (ContinuousMultilinearMap.continuous_eval_const x).comp continuous_toContinuousMultilinearMap
+instance instContinuousEvalConst : ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F :=
+  .of_continuous_forget continuous_toContinuousMultilinearMap
+
+@[deprecated (since := "2024-10-05")]
+protected alias continuous_eval_const := continuous_eval_const
 
-theorem continuous_coe_fun :
-    Continuous (DFunLike.coe : E [⋀^ι]→L[𝕜] F → (ι → E) → F) :=
-  continuous_pi continuous_eval_const
+@[deprecated (since := "2024-10-05")]
+protected alias continuous_coe_fun := continuous_coeFun
 
 instance instT2Space [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F) :=
-  .of_injective_continuous DFunLike.coe_injective continuous_coe_fun
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
 
-instance instT3Space [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F) :=
-  letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
-  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+instance instT3Space [T2Space F] : T3Space (E [⋀^ι]→L[𝕜] F) :=
   inferInstance
 
 section RestrictScalars
diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
index baf4b78201f9a..8599967f6f408 100644
--- a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
+++ b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.ContinuousEvalConst
 
 /-!
 # Topology on continuous multilinear maps
@@ -152,6 +153,11 @@ end UniformAddGroup
 
 variable [TopologicalSpace F] [TopologicalAddGroup F]
 
+instance instTopologicalAddGroup : TopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F) :=
+  letI := TopologicalAddGroup.toUniformSpace F
+  haveI := comm_topologicalAddGroup_is_uniform (G := F)
+  inferInstance
+
 instance instContinuousConstSMul
     {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
     ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) := by
@@ -188,20 +194,21 @@ theorem hasBasis_nhds_zero :
 
 variable [∀ i, ContinuousSMul 𝕜 (E i)]
 
-theorem continuous_eval_const (x : Π i, E i) :
-    Continuous fun p : ContinuousMultilinearMap 𝕜 E F ↦ p x := by
-  letI := TopologicalAddGroup.toUniformSpace F
-  haveI := comm_topologicalAddGroup_is_uniform (G := F)
-  exact (uniformContinuous_eval_const x).continuous
+instance : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
+  continuous_eval_const x :=
+    let _ := TopologicalAddGroup.toUniformSpace F
+    have _ := comm_topologicalAddGroup_is_uniform (G := F)
+    (uniformContinuous_eval_const x).continuous
 
+@[deprecated (since := "2024-10-05")] protected alias continuous_eval_const := continuous_eval_const
 @[deprecated (since := "2024-04-10")] alias continuous_eval_left := continuous_eval_const
-
-theorem continuous_coe_fun :
-    Continuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) :=
-  continuous_pi continuous_eval_const
+@[deprecated (since := "2024-10-05")] protected alias continuous_coe_fun := continuous_coeFun
 
 instance instT2Space [T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F) :=
-  .of_injective_continuous DFunLike.coe_injective continuous_coe_fun
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
+
+instance instT3Space [T2Space F] : T3Space (ContinuousMultilinearMap 𝕜 E F) :=
+  inferInstance
 
 section RestrictScalars
 
diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
index 8e988265fd745..3652ce13c16e1 100644
--- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean
+++ b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.ContinuousEvalConst
 
 /-!
 # Strong topologies on the space of continuous linear maps
@@ -151,12 +152,19 @@ instance instTopologicalAddGroup [TopologicalSpace F] [TopologicalAddGroup F]
   haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
   infer_instance
 
+theorem continuousEvalConst [TopologicalSpace F] [TopologicalAddGroup F]
+    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
+    ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F where
+  continuous_eval_const x := by
+    letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
+    haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+    exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
+      (embedding_coeFn σ F 𝔖).continuous
+
 theorem t2Space [TopologicalSpace F] [TopologicalAddGroup F] [T2Space F]
-    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) := by
-  letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
-  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
-  haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
-  exact (embedding_coeFn σ F 𝔖).t2Space
+    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) :=
+  have := continuousEvalConst σ F 𝔖 h𝔖
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
 
 instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
@@ -321,11 +329,13 @@ instance uniformSpace [UniformSpace F] [UniformAddGroup F] : UniformSpace (E →
 instance uniformAddGroup [UniformSpace F] [UniformAddGroup F] : UniformAddGroup (E →SL[σ] F) :=
   UniformConvergenceCLM.instUniformAddGroup σ F _
 
-instance [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] :
-    T2Space (E →SL[σ] F) :=
-  UniformConvergenceCLM.t2Space σ F _
-    (Set.eq_univ_of_forall fun x =>
-      Set.mem_sUnion_of_mem (Set.mem_singleton x) (isVonNBounded_singleton x))
+instance instContinuousEvalConst [TopologicalSpace F] [TopologicalAddGroup F]
+    [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F :=
+  UniformConvergenceCLM.continuousEvalConst σ F _ Bornology.isVonNBounded_covers
+
+instance instT2Space [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E]
+    [T2Space F] : T2Space (E →SL[σ] F) :=
+  UniformConvergenceCLM.t2Space σ F _ Bornology.isVonNBounded_covers
 
 protected theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [TopologicalAddGroup F]
     {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean
index 0338dd8e2d361..c1bc6c33fb9ab 100644
--- a/Mathlib/Topology/CompactOpen.lean
+++ b/Mathlib/Topology/CompactOpen.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton
 -/
-import Mathlib.Topology.ContinuousMap.Basic
+import Mathlib.Topology.ContinuousMap.ContinuousEval
 
 /-!
 # The compact-open topology
@@ -160,27 +160,24 @@ section Ev
 
 /-- The evaluation map `C(X, Y) × X → Y` is continuous
 if `X, Y` is a locally compact pair of spaces. -/
-@[continuity]
-theorem continuous_eval [LocallyCompactPair X Y] : Continuous fun p : C(X, Y) × X => p.1 p.2 := by
-  simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
-  rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
-  rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
-  filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
+instance [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y where
+  continuous_eval := by
+    simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
+    rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
+    rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
+    filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
 
-/-- Evaluation of a continuous map `f` at a point `x` is continuous in `f`.
+@[deprecated (since := "2024-10-01")] protected alias continuous_eval := continuous_eval
 
-Porting note: merged `continuous_eval_const` with `continuous_eval_const'` removing unneeded
-assumptions. -/
-@[continuity]
-theorem continuous_eval_const (a : X) : Continuous fun f : C(X, Y) => f a :=
-  continuous_def.2 fun U hU ↦ by simpa using isOpen_setOf_mapsTo (isCompact_singleton (x := a)) hU
+instance : ContinuousEvalConst C(X, Y) X Y where
+  continuous_eval_const x :=
+    continuous_def.2 fun U hU ↦ by simpa using isOpen_setOf_mapsTo isCompact_singleton hU
 
-/-- Coercion from `C(X, Y)` with compact-open topology to `X → Y` with pointwise convergence
-topology is a continuous map.
+@[deprecated (since := "2024-10-01")] protected alias continuous_eval_const := continuous_eval_const
 
-Porting note: merged `continuous_coe` with `continuous_coe'` removing unneeded assumptions. -/
+@[deprecated continuous_coeFun (since := "2024-10-01")]
 theorem continuous_coe : Continuous ((⇑) : C(X, Y) → (X → Y)) :=
-  continuous_pi continuous_eval_const
+  continuous_coeFun
 
 lemma isClosed_setOf_mapsTo {t : Set Y} (ht : IsClosed t) (s : Set X) :
     IsClosed {f : C(X, Y) | MapsTo f s t} :=
@@ -192,7 +189,7 @@ lemma isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) :
 
 @[norm_cast]
 lemma specializes_coe {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g := by
-  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coe⟩
+  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
   suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
     simpa [specializes_iff_pure, nhds_compactOpen]
   exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)
@@ -202,7 +199,7 @@ lemma inseparable_coe {f g : C(X, Y)} : Inseparable (f : X → Y) g ↔ Insepara
   simp only [inseparable_iff_specializes_and, specializes_coe]
 
 instance [T0Space Y] : T0Space C(X, Y) :=
-  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe
+  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun
 
 instance [R0Space Y] : R0Space C(X, Y) where
   specializes_symmetric f g h := by
@@ -210,10 +207,10 @@ instance [R0Space Y] : R0Space C(X, Y) where
     exact h.symm
 
 instance [T1Space Y] : T1Space C(X, Y) :=
-  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe
+  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun
 
 instance [R1Space Y] : R1Space C(X, Y) :=
-  .of_continuous_specializes_imp continuous_coe fun _ _ ↦ specializes_coe.1
+  .of_continuous_specializes_imp continuous_coeFun fun _ _ ↦ specializes_coe.1
 
 instance [T2Space Y] : T2Space C(X, Y) := inferInstance
 
@@ -388,7 +385,8 @@ theorem continuous_uncurry [LocallyCompactSpace X] [LocallyCompactSpace Y] :
     Continuous (uncurry : C(X, C(Y, Z)) → C(X × Y, Z)) := by
   apply continuous_of_continuous_uncurry
   rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
-  apply continuous_eval.comp (continuous_eval.prodMap continuous_id)
+  dsimp
+  exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd
 
 /-- The family of constant maps: `Y → C(X, Y)` as a continuous map. -/
 def const' : C(Y, C(X, Y)) :=
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
index 644fcb694b3a8..79728920da20b 100644
--- a/Mathlib/Topology/Connected/PathConnected.lean
+++ b/Mathlib/Topology/Connected/PathConnected.lean
@@ -198,14 +198,14 @@ compact-open topology on the space `C(I,X)` of continuous maps from `I` to `X`.
 instance topologicalSpace : TopologicalSpace (Path x y) :=
   TopologicalSpace.induced ((↑) : _ → C(I, X)) ContinuousMap.compactOpen
 
-theorem continuous_eval : Continuous fun p : Path x y × I => p.1 p.2 :=
-  ContinuousMap.continuous_eval.comp <|
-    (continuous_induced_dom (α := Path x y)).prodMap continuous_id
+instance : ContinuousEval (Path x y) I X := .of_continuous_forget continuous_induced_dom
 
-@[continuity]
+@[deprecated (since := "2024-10-04")] protected alias continuous_eval := continuous_eval
+
+@[deprecated Continuous.eval (since := "2024-10-04")]
 theorem _root_.Continuous.path_eval {Y} [TopologicalSpace Y] {f : Y → Path x y} {g : Y → I}
-    (hf : Continuous f) (hg : Continuous g) : Continuous fun y => f y (g y) :=
-  Continuous.comp continuous_eval (hf.prod_mk hg)
+    (hf : Continuous f) (hg : Continuous g) : Continuous fun y => f y (g y) := by
+  continuity
 
 theorem continuous_uncurry_iff {Y} [TopologicalSpace Y] {g : Y → Path x y} :
     Continuous ↿g ↔ Continuous g :=
@@ -427,7 +427,7 @@ theorem symm_continuous_family {ι : Type*} [TopologicalSpace ι]
 
 @[continuity]
 theorem continuous_symm : Continuous (symm : Path x y → Path y x) :=
-  continuous_uncurry_iff.mp <| symm_continuous_family _ (continuous_fst.path_eval continuous_snd)
+  continuous_uncurry_iff.mp <| symm_continuous_family _ (continuous_fst.eval continuous_snd)
 
 @[continuity]
 theorem continuous_uncurry_extend_of_continuous_family {ι : Type*} [TopologicalSpace ι]
diff --git a/Mathlib/Topology/ContinuousEvalConst.lean b/Mathlib/Topology/ContinuousEvalConst.lean
new file mode 100644
index 0000000000000..89cde94b440c3
--- /dev/null
+++ b/Mathlib/Topology/ContinuousEvalConst.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Constructions
+
+/-!
+# Bundled morphisms with continuous evaluation at a point
+
+In this file we define a typeclass
+saying that `F` is a type of bundled morphisms (in the sense of `DFunLike`)
+with a topology on `F` such that evaluation at a point is continuous in `f : F`.
+
+## Implementation Notes
+
+For now, we define the typeclass for non-dependent bundled functions only.
+Whenever we add a type of bundled dependent functions with a topology having this property,
+we may decide to generalize from `FunLike` to `DFunLike`.
+-/
+
+open scoped Topology
+open Filter
+
+/-- A typeclass saying that `F` is a type of bundled morphisms (in the sense of `DFunLike`)
+with a topology on `F` such that evaluation at a point is continuous in `f : F`. -/
+class ContinuousEvalConst (F : Type*) (α X : outParam Type*) [FunLike F α X]
+    [TopologicalSpace F] [TopologicalSpace X] : Prop where
+  continuous_eval_const (x : α) : Continuous fun f : F ↦ f x
+
+export ContinuousEvalConst (continuous_eval_const)
+
+section ContinuousEvalConst
+
+variable {F α X Z : Type*} [FunLike F α X] [TopologicalSpace F] [TopologicalSpace X]
+  [ContinuousEvalConst F α X] [TopologicalSpace Z] {f : Z → F} {s : Set Z} {z : Z}
+
+-- TODO: docstring
+theorem ContinuousEvalConst.of_continuous_forget {F' : Type*} [FunLike F' α X] [TopologicalSpace F']
+    {f : F' → F} (hc : Continuous f) (hf : ∀ g, ⇑(f g) = g := by intro; rfl) :
+    ContinuousEvalConst F' α X where
+  continuous_eval_const x := by simpa only [← hf] using (continuous_eval_const x).comp hc
+
+@[continuity, fun_prop]
+theorem Continuous.eval_const (hf : Continuous f) (x : α) : Continuous (f · x) :=
+  (continuous_eval_const x).comp hf
+
+theorem continuous_coeFun : Continuous (DFunLike.coe : F → α → X) :=
+  continuous_pi continuous_eval_const
+
+protected theorem Continuous.coeFun (hf : Continuous f) : Continuous fun z ↦ ⇑(f z) :=
+  continuous_pi hf.eval_const
+
+theorem Filter.Tendsto.eval_const {ι : Type*} {l : Filter ι} {f : ι → F} {g : F}
+    (hf : Tendsto f l (𝓝 g)) (a : α) : Tendsto (f · a) l (𝓝 (g a)) :=
+  ((continuous_id.eval_const a).tendsto _).comp hf
+
+theorem Filter.Tendsto.coeFun {ι : Type*} {l : Filter ι} {f : ι → F} {g : F}
+    (hf : Tendsto f l (𝓝 g)) : Tendsto (fun i ↦ ⇑(f i)) l (𝓝 ⇑g) :=
+  (continuous_id.coeFun.tendsto _).comp hf
+
+nonrec theorem ContinuousAt.eval_const (hf : ContinuousAt f z) (x : α) : ContinuousAt (f · x) z :=
+  hf.eval_const x
+
+nonrec theorem ContinuousAt.coeFun (hf : ContinuousAt f z) : ContinuousAt (fun z ↦ ⇑(f z)) z :=
+  hf.coeFun
+
+nonrec theorem ContinuousWithinAt.eval_const (hf : ContinuousWithinAt f s z) (x : α) :
+    ContinuousWithinAt (f · x) s z :=
+  hf.eval_const x
+
+nonrec theorem ContinuousWithinAt.coeFun (hf : ContinuousWithinAt f s z) :
+    ContinuousWithinAt (fun z ↦ ⇑(f z)) s z :=
+  hf.coeFun
+
+theorem ContinuousOn.eval_const (hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s :=
+  fun z hz ↦ (hf z hz).eval_const x
+
+theorem ContinuousOn.coeFun (hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s :=
+  fun z hz ↦ (hf z hz).eval_const x
+
+end ContinuousEvalConst
diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean
index 4e62f17e049be..f38ec169823f5 100644
--- a/Mathlib/Topology/ContinuousMap/Algebra.lean
+++ b/Mathlib/Topology/ContinuousMap/Algebra.lean
@@ -372,25 +372,25 @@ instance [CommGroup β] [TopologicalGroup β] : TopologicalGroup C(α, β) where
       uniformContinuous_inv.comp_tendstoUniformlyOn
         (tendsto_iff_forall_compact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)
 
--- TODO: rewrite the next three lemmas for products and deduce sum case via `to_additive`, once
--- definition of `tprod` is in place
-/-- If `α` is locally compact, and an infinite sum of functions in `C(α, β)`
-converges to `g` (for the compact-open topology), then the pointwise sum converges to `g x` for
-all `x ∈ α`. -/
-theorem hasSum_apply {γ : Type*} [AddCommMonoid β] [ContinuousAdd β]
-    {f : γ → C(α, β)} {g : C(α, β)} (hf : HasSum f g) (x : α) :
-    HasSum (fun i : γ => f i x) (g x) := by
-  let ev : C(α, β) →+ β := (Pi.evalAddMonoidHom _ x).comp coeFnAddMonoidHom
-  exact hf.map ev (ContinuousMap.continuous_eval_const x)
-
-theorem summable_apply [AddCommMonoid β] [ContinuousAdd β] {γ : Type*} {f : γ → C(α, β)}
-    (hf : Summable f) (x : α) : Summable fun i : γ => f i x :=
-  (hasSum_apply hf.hasSum x).summable
-
-theorem tsum_apply [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type*} {f : γ → C(α, β)}
-    (hf : Summable f) (x : α) :
-    ∑' i : γ, f i x = (∑' i : γ, f i) x :=
-  (hasSum_apply hf.hasSum x).tsum_eq
+/-- If an infinite sum of functions in `C(α, β)` converges to `g` (for the compact-open topology),
+then the pointwise sum converges to `g x` for all `x ∈ α`. -/
+@[to_additive]
+theorem hasProd_apply {γ : Type*} [CommMonoid β] [ContinuousMul β]
+    {f : γ → C(α, β)} {g : C(α, β)} (hf : HasProd f g) (x : α) :
+    HasProd (fun i : γ => f i x) (g x) := by
+  let ev : C(α, β) →* β := (Pi.evalMonoidHom _ x).comp coeFnMonoidHom
+  exact hf.map ev (continuous_eval_const x)
+
+@[to_additive]
+theorem multipliable_apply [CommMonoid β] [ContinuousMul β] {γ : Type*} {f : γ → C(α, β)}
+    (hf : Multipliable f) (x : α) : Multipliable fun i : γ => f i x :=
+  (hasProd_apply hf.hasProd x).multipliable
+
+@[to_additive]
+theorem tprod_apply [T2Space β] [CommMonoid β] [ContinuousMul β] {γ : Type*} {f : γ → C(α, β)}
+    (hf : Multipliable f) (x : α) :
+    ∏' i : γ, f i x = (∏' i : γ, f i) x :=
+  (hasProd_apply hf.hasProd x).tprod_eq
 
 end ContinuousMap
 
diff --git a/Mathlib/Topology/ContinuousMap/ContinuousEval.lean b/Mathlib/Topology/ContinuousMap/ContinuousEval.lean
new file mode 100644
index 0000000000000..5098672f69550
--- /dev/null
+++ b/Mathlib/Topology/ContinuousMap/ContinuousEval.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.ContinuousMap.Basic
+import Mathlib.Topology.ContinuousEvalConst
+
+/-!
+# Bundled maps with evaluation continuous in both variables
+
+In this file we define a class `ContinuousEval F X Y`
+saying that `F` is a bundled morphism class (in the sense of `FunLike`)
+with a topology such that `fun (f, x) : F × X ↦ f x` is a continuous function.
+-/
+
+open scoped Topology
+open Filter
+
+/-- A typeclass saying that `F` is a bundled morphism class (in the sense of `FunLike`)
+with a topology such that `fun (f, x) : F × X ↦ f x` is a continuous function. -/
+class ContinuousEval (F : Type*) (X Y : outParam Type*) [FunLike F X Y]
+    [TopologicalSpace F] [TopologicalSpace X] [TopologicalSpace Y] : Prop where
+  /-- Evaluation of a bundled morphism at a point is continuous in both variables. -/
+  continuous_eval : Continuous fun fx : F × X ↦ fx.1 fx.2
+
+export ContinuousEval (continuous_eval)
+
+variable {F X Y Z : Type*} [FunLike F X Y]
+  [TopologicalSpace F] [TopologicalSpace X] [TopologicalSpace Y] [ContinuousEval F X Y]
+  [TopologicalSpace Z] {f : Z → F} {g : Z → X} {s : Set Z} {z : Z}
+
+@[continuity, fun_prop]
+protected theorem Continuous.eval (hf : Continuous f) (hg : Continuous g) :
+    Continuous fun z ↦ f z (g z) :=
+  continuous_eval.comp (hf.prod_mk hg)
+
+theorem ContinuousEval.of_continuous_forget {F' : Type*} [FunLike F' X Y] [TopologicalSpace F']
+    {f : F' → F} (hc : Continuous f) (hf : ∀ g, ⇑(f g) = g := by intro; rfl) :
+    ContinuousEval F' X Y where
+  continuous_eval := by simpa only [← hf] using hc.fst'.eval continuous_snd
+
+instance (priority := 100) ContinuousEval.toContinuousMapClass : ContinuousMapClass F X Y where
+  map_continuous _ := continuous_const.eval continuous_id
+
+instance (priority := 100) ContinuousEval.toContinuousEvalConst : ContinuousEvalConst F X Y where
+  continuous_eval_const _ := continuous_id.eval continuous_const
+
+protected theorem Filter.Tendsto.eval {α : Type*} {l : Filter α} {f : α → F} {f₀ : F}
+    {g : α → X} {x₀ : X} (hf : Tendsto f l (𝓝 f₀)) (hg : Tendsto g l (𝓝 x₀)) :
+    Tendsto (fun a ↦ f a (g a)) l (𝓝 (f₀ x₀)) :=
+  (ContinuousEval.continuous_eval.tendsto _).comp (hf.prod_mk_nhds hg)
+
+protected nonrec theorem ContinuousAt.eval (hf : ContinuousAt f z) (hg : ContinuousAt g z) :
+    ContinuousAt (fun z ↦ f z (g z)) z :=
+  hf.eval hg
+
+protected nonrec theorem ContinuousWithinAt.eval (hf : ContinuousWithinAt f s z)
+    (hg : ContinuousWithinAt g s z) : ContinuousWithinAt (fun z ↦ f z (g z)) s z :=
+  hf.eval hg
+
+protected theorem ContinuousOn.eval (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
+    ContinuousOn (fun z ↦ f z (g z)) s :=
+  fun z hz ↦ (hf z hz).eval (hg z hz)
diff --git a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
index 5fa65e8b7c342..575b4e26ad07c 100644
--- a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
+++ b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
@@ -85,15 +85,25 @@ lemma embedding_toContinuousMap : Embedding ((↑) : C(X, R)₀ → C(X, R)) whe
   inj _ _ h := ext fun x ↦ congr($(h) x)
 
 instance [T0Space R] : T0Space C(X, R)₀ := embedding_toContinuousMap.t0Space
+instance [R0Space R] : R0Space C(X, R)₀ := embedding_toContinuousMap.r0Space
 instance [T1Space R] : T1Space C(X, R)₀ := embedding_toContinuousMap.t1Space
+instance [R1Space R] : R1Space C(X, R)₀ := embedding_toContinuousMap.r1Space
 instance [T2Space R] : T2Space C(X, R)₀ := embedding_toContinuousMap.t2Space
+instance [RegularSpace R] : RegularSpace C(X, R)₀ := embedding_toContinuousMap.regularSpace
+instance [T3Space R] : T3Space C(X, R)₀ := embedding_toContinuousMap.t3Space
+
+instance instContinuousEvalConst : ContinuousEvalConst C(X, R)₀ X R :=
+  .of_continuous_forget embedding_toContinuousMap.continuous
+
+instance instContinuousEval [LocallyCompactPair X R] : ContinuousEval C(X, R)₀ X R :=
+  .of_continuous_forget embedding_toContinuousMap.continuous
 
 lemma closedEmbedding_toContinuousMap [T1Space R] :
     ClosedEmbedding ((↑) : C(X, R)₀ → C(X, R)) where
   toEmbedding := embedding_toContinuousMap
   isClosed_range := by
     rw [range_toContinuousMap]
-    exact isClosed_singleton.preimage <| ContinuousMap.continuous_eval_const 0
+    exact isClosed_singleton.preimage <| continuous_eval_const 0
 
 @[fun_prop]
 lemma continuous_comp_left {X Y Z : Type*} [TopologicalSpace X]
diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean
index 15648773fa822..a971740b0806e 100644
--- a/Mathlib/Topology/Homotopy/HSpaces.lean
+++ b/Mathlib/Topology/Homotopy/HSpaces.lean
@@ -212,7 +212,7 @@ def delayReflRight (θ : I) (γ : Path x y) : Path x y where
 
 theorem continuous_delayReflRight : Continuous fun p : I × Path x y => delayReflRight p.1 p.2 :=
   continuous_uncurry_iff.mp <|
-    (continuous_snd.comp continuous_fst).path_eval <|
+    (continuous_snd.comp continuous_fst).eval <|
       continuous_qRight.comp <| continuous_snd.prod_mk <| continuous_fst.comp continuous_fst
 
 theorem delayReflRight_zero (γ : Path x y) : delayReflRight 0 γ = γ.trans (Path.refl y) := by
diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
index daaa41db02500..e91805dc36b4f 100644
--- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean
+++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
@@ -111,6 +111,11 @@ theorem ext (f g : Ω^ N X x) (H : ∀ y, f y = g y) : f = g :=
 theorem mk_apply (f : C(I^N, X)) (H y) : (⟨f, H⟩ : Ω^ N X x) y = f y :=
   rfl
 
+instance instContinuousEval : ContinuousEval (Ω^ N X x) (I^N) X :=
+  .of_continuous_forget continuous_subtype_val
+
+instance instContinuousEvalConst : ContinuousEvalConst (Ω^ N X x) (I^N) X := inferInstance
+
 /-- Copy of a `GenLoop` with a new map from the unit cube equal to the old one.
   Useful to fix definitional equalities. -/
 def copy (f : Ω^ N X x) (g : (I^N) → X) (h : g = f) : Ω^ N X x :=
@@ -184,8 +189,8 @@ def toLoop (i : N) (p : Ω^ N X x) : Ω (Ω^ { j // j ≠ i } X x) const where
 theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
   Path.continuous_uncurry_iff.1 <|
     Continuous.subtype_mk
-      (ContinuousMap.continuous_eval.comp <|
-        Continuous.prodMap
+      (continuous_eval.comp <|
+        Continuous.prod_map
           (ContinuousMap.continuous_curry.comp <|
             (ContinuousMap.continuous_comp_left _).comp continuous_subtype_val)
           continuous_id)
@@ -373,7 +378,6 @@ def genLoopHomeoOfIsEmpty (N x) [IsEmpty N] : Ω^ N X x ≃ₜ X where
   invFun y := ⟨ContinuousMap.const _ y, fun _ ⟨i, _⟩ => isEmptyElim i⟩
   left_inv f := by ext; exact congr_arg f (Subsingleton.elim _ _)
   right_inv _ := rfl
-  continuous_toFun := (ContinuousMap.continuous_eval_const (0 : N → I)).comp continuous_induced_dom
   continuous_invFun := ContinuousMap.const'.2.subtype_mk _
 
 /-- The homotopy "group" indexed by an empty type is in bijection with
diff --git a/Mathlib/Topology/Homotopy/Path.lean b/Mathlib/Topology/Homotopy/Path.lean
index 254ed2b7f70dc..a5ad060e6071e 100644
--- a/Mathlib/Topology/Homotopy/Path.lean
+++ b/Mathlib/Topology/Homotopy/Path.lean
@@ -188,15 +188,7 @@ def reparam (p : Path x₀ x₁) (f : I → I) (hf : Continuous f) (hf₀ : f 0
     · rw [Set.mem_singleton_iff] at hx
       rw [hx]
       simp [hf₁]
-  continuous_toFun := by
-    -- Porting note: was `continuity` in auto-param
-    refine continuous_const.path_eval ?_
-    apply Continuous.subtype_mk
-    apply Continuous.add <;> apply Continuous.mul
-    · exact continuous_induced_dom.comp (unitInterval.continuous_symm.comp continuous_fst)
-    · continuity
-    · continuity
-    · continuity
+  continuous_toFun := by fun_prop
 
 /-- Suppose `F : Homotopy p q`. Then we have a `Homotopy p.symm q.symm` by reversing the second
 argument.