feat(CompactOpen): unify 2 continuous_eval lemmas (#9264)

Introduce a typeclass `LocallyCompactPair` that allows us to unify different versions of `ContinuousMap.continuous_eval` and similar lemmas.

Mathlib/Topology/CompactOpen.lean

@@ -32,9 +32,8 @@ compact-open, curry, function space
 -/
 
 
-open Set
-
-open Topology
+open Set Filter TopologicalSpace
+open scoped Topology
 
 namespace ContinuousMap
 
@@ -91,6 +90,23 @@ protected theorem isOpen_gen {s : Set α} (hs : IsCompact s) {u : Set β} (hu :
   TopologicalSpace.GenerateOpen.basic _ (by dsimp [mem_setOf_eq]; tauto)
 #align continuous_map.is_open_gen ContinuousMap.isOpen_gen
 
+lemma isOpen_setOf_mapsTo {K : Set α} (hK : IsCompact K) {U : Set β} (hU : IsOpen U) :
+    IsOpen {f : C(α, β) | MapsTo f K U} := by
+  simpa only [mapsTo'] using ContinuousMap.isOpen_gen hK hU
+
+lemma eventually_mapsTo {f : C(α, β)} {K U} (hK : IsCompact K) (hU : IsOpen U) (h : MapsTo f K U) :
+    ∀ᶠ g : C(α, β) in 𝓝 f, MapsTo g K U :=
+  (isOpen_setOf_mapsTo hK hU).mem_nhds h
+
+lemma tendsto_nhds_compactOpen {α : Type*} {l : Filter α} {f : α → C(β, γ)} {g : C(β, γ)} :
+    Tendsto f l (𝓝 g) ↔
+      ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → ∀ᶠ a in l, MapsTo (f a) K U := by
+  simp_rw [compactOpen_eq, tendsto_nhds_generateFrom_iff, forall_image2_iff, mapsTo']; rfl
+
+lemma continuous_compactOpen {f : α → C(β, γ)} :
+    Continuous f ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → IsOpen {x | MapsTo (f x) K U} := by
+  simp_rw [compactOpen_eq, continuous_generateFrom_iff, forall_image2_iff, mapsTo']; rfl
+
 section Functorial
 
 variable (g : C(β, γ))
@@ -136,29 +152,20 @@ theorem continuous_comp_left : Continuous (fun g => g.comp f : C(β, γ) → C(
 
 /-- Composition is a continuous map from `C(α, β) × C(β, γ)` to `C(α, γ)`, provided that `β` is
   locally compact. This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's *Topologie Générale*. -/
-theorem continuous_comp' [LocallyCompactSpace β] :
-    Continuous fun x : C(α, β) × C(β, γ) => x.2.comp x.1 :=
-  continuous_generateFrom_iff.2
-    (by
-      rintro M ⟨K, hK, U, hU, rfl⟩
-      conv =>
-        congr
-        rw [CompactOpen.gen, preimage_setOf_eq]
-        --congr
-        ext; dsimp [setOf]
-        rw [image_comp, image_subset_iff]
-      rw [isOpen_iff_forall_mem_open]
-      rintro ⟨φ₀, ψ₀⟩ H
-      obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between (hK.image φ₀.2) (hU.preimage ψ₀.2) H
-      use { φ : C(α, β) | φ '' K ⊆ interior L } ×ˢ { ψ : C(β, γ) | ψ '' L ⊆ U }
-      -- porting note: typing hint `: φ '' K ⊆ interior L` wasn't previously required
-      use fun ⟨φ, ψ⟩ ⟨(hφ : φ '' K ⊆ interior L), hψ⟩ =>
-        subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)
-      use (ContinuousMap.isOpen_gen hK isOpen_interior).prod (ContinuousMap.isOpen_gen hL hU)
-      exact mem_prod.mpr ⟨hKL, image_subset_iff.mpr hLU⟩)
+theorem continuous_comp' [LocallyCompactPair β γ] :
+    Continuous fun x : C(α, β) × C(β, γ) => x.2.comp x.1 := by
+  simp_rw [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen]
+  intro ⟨f, g⟩ K hK U hU (hKU : MapsTo (g ∘ f) K U)
+  obtain ⟨L, hKL, hLc, hLU⟩ : ∃ L ∈ 𝓝ˢ (f '' K), IsCompact L ∧ MapsTo g L U :=
+    exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU
+      (mapsTo_image_iff.2 hKU)
+  rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo'] at hKL
+  exact ((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
+    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
+      hg'.comp <| hf'.mono_right interior_subset
 #align continuous_map.continuous_comp' ContinuousMap.continuous_comp'
 
-theorem continuous.comp' {X : Type*} [TopologicalSpace X] [LocallyCompactSpace β] {f : X → C(α, β)}
+theorem continuous.comp' {X : Type*} [TopologicalSpace X] [LocallyCompactPair β γ] {f : X → C(α, β)}
     {g : X → C(β, γ)} (hf : Continuous f) (hg : Continuous g) :
     Continuous fun x => (g x).comp (f x) :=
   continuous_comp'.comp (hf.prod_mk hg : Continuous fun x => (f x, g x))
@@ -168,30 +175,18 @@ end Functorial
 
 section Ev
 
-/-- The evaluation map `C(α, β) × α → β` is continuous if `α` is locally compact.
-
-See also `ContinuousMap.continuous_eval` -/
-theorem continuous_eval' [LocallyCompactSpace α] : Continuous fun p : C(α, β) × α => p.1 p.2 :=
-  continuous_iff_continuousAt.mpr fun ⟨f, x⟩ n hn =>
-    let ⟨v, vn, vo, fxv⟩ := mem_nhds_iff.mp hn
-    have : v ∈ 𝓝 (f x) := IsOpen.mem_nhds vo fxv
-    let ⟨s, hs, sv, sc⟩ :=
-      LocallyCompactSpace.local_compact_nhds x (f ⁻¹' v) (f.continuous.tendsto x this)
-    let ⟨u, us, uo, xu⟩ := mem_nhds_iff.mp hs
-    show (fun p : C(α, β) × α => p.1 p.2) ⁻¹' n ∈ 𝓝 (f, x) from
-      let w := CompactOpen.gen s v ×ˢ u
-      have : w ⊆ (fun p : C(α, β) × α => p.1 p.2) ⁻¹' n := fun ⟨f', x'⟩ ⟨hf', hx'⟩ =>
-        vn <| hf' <| mem_image_of_mem f' (us hx')
-        --Porting note: The following `calc` block fails here.
-        --calc
-        --  f' x' ∈ f' '' s := mem_image_of_mem f' (us hx')
-        --  _ ⊆ v := hf'
-        --  _ ⊆ n := vn
-
-      have : IsOpen w := (ContinuousMap.isOpen_gen sc vo).prod uo
-      have : (f, x) ∈ w := ⟨image_subset_iff.mpr sv, xu⟩
-      mem_nhds_iff.mpr ⟨w, by assumption, by assumption, by assumption⟩
-#align continuous_map.continuous_eval' ContinuousMap.continuous_eval'
+/-- The evaluation map `C(α, β) × α → β` is continuous
+if `α, β` is a locally compact pair of spaces. -/
+@[continuity]
+theorem continuous_eval [LocallyCompactPair α β] : Continuous fun p : C(α, β) × α => 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
+#align continuous_map.continuous_eval' ContinuousMap.continuous_eval
+#align continuous_map.continuous_eval ContinuousMap.continuous_eval
+
+@[deprecated] alias continuous_eval' := continuous_eval
 
 /-- Evaluation of a continuous map `f` at a point `a` is continuous in `f`.
 
@@ -395,13 +390,13 @@ theorem continuous_curry [LocallyCompactSpace (α × β)] :
   apply continuous_of_continuous_uncurry
   apply continuous_of_continuous_uncurry
   rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']
-  exact continuous_eval'
+  exact continuous_eval
 #align continuous_map.continuous_curry ContinuousMap.continuous_curry
 
 /-- The uncurried form of a continuous map `α → C(β, γ)` is a continuous map `α × β → γ`. -/
 theorem continuous_uncurry_of_continuous [LocallyCompactSpace β] (f : C(α, C(β, γ))) :
     Continuous (Function.uncurry fun x y => f x y) :=
-  continuous_eval'.comp <| f.continuous.prod_map continuous_id
+  continuous_eval.comp <| f.continuous.prod_map continuous_id
 #align continuous_map.continuous_uncurry_of_continuous ContinuousMap.continuous_uncurry_of_continuous
 
 /-- The uncurried form of a continuous map `α → C(β, γ)` as a continuous map `α × β → γ` (if `β` is
@@ -417,7 +412,7 @@ theorem continuous_uncurry [LocallyCompactSpace α] [LocallyCompactSpace β] :
     Continuous (uncurry : C(α, C(β, γ)) → C(α × β, γ)) := by
   apply continuous_of_continuous_uncurry
   rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
-  apply continuous_eval'.comp (continuous_eval'.prod_map continuous_id)
+  apply continuous_eval.comp (continuous_eval.prod_map continuous_id)
 #align continuous_map.continuous_uncurry ContinuousMap.continuous_uncurry
 
 /-- The family of constant maps: `β → C(α, β)` as a continuous map. -/

Mathlib/Topology/Compactness/Compact.lean

@@ -191,20 +191,31 @@ theorem IsCompact.elim_finite_subcover {ι : Type v} (hs : IsCompact s) (U : ι
     (directed_of_isDirected_le fun _ _ h => biUnion_subset_biUnion_left h)
 #align is_compact.elim_finite_subcover IsCompact.elim_finite_subcover
 
+lemma IsCompact.elim_nhds_subcover_nhdsSet' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
+    (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ t : Finset s, (⋃ x ∈ t, U x.1 x.2) ∈ 𝓝ˢ s := by
+  rcases hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
+    fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with ⟨t, hst⟩
+  refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
+  rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩
+  refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)
+  exact mem_interior_iff_mem_nhds.1 hy
+
+lemma IsCompact.elim_nhds_subcover_nhdsSet (hs : IsCompact s) {U : X → Set X}
+    (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ (⋃ x ∈ t, U x) ∈ 𝓝ˢ s :=
+  let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
+  ⟨t.image (↑), fun x hx =>
+    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
+    hyx ▸ y.2,
+    by rwa [Finset.set_biUnion_finset_image]⟩
+
 theorem IsCompact.elim_nhds_subcover' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
     (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) : ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U (x : s) x.2 :=
-  (hs.elim_finite_subcover (fun x : s => interior (U x x.2)) (fun _ => isOpen_interior) fun x hx =>
-        mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩).imp
-    fun _t ht => ht.trans <| iUnion₂_mono fun _ _ => interior_subset
+  (hs.elim_nhds_subcover_nhdsSet' U hU).imp fun _ ↦ subset_of_mem_nhdsSet
 #align is_compact.elim_nhds_subcover' IsCompact.elim_nhds_subcover'
 
 theorem IsCompact.elim_nhds_subcover (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
     ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x :=
-  let ⟨t, ht⟩ := hs.elim_nhds_subcover' (fun x _ => U x) hU
-  ⟨t.image (↑), fun x hx =>
-    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
-    hyx ▸ y.2,
-    by rwa [Finset.set_biUnion_finset_image]⟩
+  (hs.elim_nhds_subcover_nhdsSet hU).imp fun _ h ↦ h.imp_right subset_of_mem_nhdsSet
 #align is_compact.elim_nhds_subcover IsCompact.elim_nhds_subcover
 
 /-- The neighborhood filter of a compact set is disjoint with a filter `l` if and only if the

Mathlib/Topology/Compactness/LocallyCompact.lean

@@ -149,6 +149,36 @@ instance Function.locallyCompactSpace [LocallyCompactSpace Y] [CompactSpace Y] :
 
 end Pi
 
+/-- We say that `X` and `Y` are a locally compact pair of topological spaces,
+if for any continuous map `f : X → Y`, a point `x : X`, and a neighbourhood `s ∈ 𝓝 (f x)`,
+there exists a compact neighbourhood `K ∈ 𝓝 x` such that `f` maps `K` to `s`.
+
+This is a technical assumption that appears in several theorems,
+most notably in `ContinuousMap.continuous_comp'` and `ContinuousMap.continuous_eval`.
+It is satisfied in two cases:
+
+- if `X` is a locally compact topological space, for obvious reasons;
+- if `X` is a weakly locally compact topological space and `Y` is a Hausdorff space;
+  this fact is a simple generalization of the theorem
+  saying that a weakly locally compact Hausdorff topological space is locally compact.
+-/
+class LocallyCompactPair (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] : Prop where
+  /-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces
+  and `s : Set Y` is a neighbourhood of `f x`, `x : X`,
+  then there exists a compact neighbourhood `K` of `x` such that `f` maps `K` to `s`. -/
+  exists_mem_nhds_isCompact_mapsTo : ∀ {f : X → Y} {x : X} {s : Set Y},
+    Continuous f → s ∈ 𝓝 (f x) → ∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s
+
+export LocallyCompactPair (exists_mem_nhds_isCompact_mapsTo)
+
+instance (priority := 900) [LocallyCompactSpace X] : LocallyCompactPair X Y where
+  exists_mem_nhds_isCompact_mapsTo hf hs :=
+    let ⟨K, hKx, hKs, hKc⟩ := local_compact_nhds (hf.continuousAt hs); ⟨K, hKx, hKc, hKs⟩
+
+instance (priority := 100) [LocallyCompactSpace X] : WeaklyLocallyCompactSpace X where
+  exists_compact_mem_nhds (x : X) :=
+    let ⟨K, hx, _, hKc⟩ := local_compact_nhds (x := x) univ_mem; ⟨K, hKc, hx⟩
+
 /-- A reformulation of the definition of locally compact space: In a locally compact space,
   every open set containing `x` has a compact subset containing `x` in its interior. -/
 theorem exists_compact_subset [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U)
@@ -157,25 +187,29 @@ theorem exists_compact_subset [LocallyCompactSpace X] {x : X} {U : Set X} (hU :
   exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩
 #align exists_compact_subset exists_compact_subset
 
-instance (priority := 100) [LocallyCompactSpace X] : WeaklyLocallyCompactSpace X where
-  exists_compact_mem_nhds (x : X) :=
-    let ⟨K, hKc, hx, _⟩ := exists_compact_subset isOpen_univ (mem_univ x)
-    ⟨K, hKc, mem_interior_iff_mem_nhds.1 hx⟩
+/-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces,
+`K : set X` is a compact set, and `U` is an open neighbourhood of `f '' K`,
+then there exists a compact neighbourhood `L` of `K` such that `f` maps `L` to `U`.
+
+This is a generalization of `exists_mem_nhds_isCompact_mapsTo`. -/
+lemma exists_mem_nhdsSet_isCompact_mapsTo [LocallyCompactPair X Y] {f : X → Y} {K : Set X}
+    {U : Set Y} (hf : Continuous f) (hK : IsCompact K) (hU : IsOpen U) (hKU : MapsTo f K U) :
+    ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U := by
+  choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
+    exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))
+  rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩
+  exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂ fun x hx ↦
+    hVU x (hsK x hx)⟩
 
 /-- In a locally compact space, for every containment `K ⊆ U` of a compact set `K` in an open
   set `U`, there is a compact neighborhood `L` such that `K ⊆ L ⊆ U`: equivalently, there is a
   compact `L` such that `K ⊆ interior L` and `L ⊆ U`.
   See also `exists_compact_closed_between`, in which one guarantees additionally that `L` is closed
   if the space is regular. -/
-theorem exists_compact_between [hX : LocallyCompactSpace X] {K U : Set X} (hK : IsCompact K)
-    (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U := by
-  choose V hVc hxV hKV using fun x : K => exists_compact_subset hU (h_KU x.2)
-  have : K ⊆ ⋃ x, interior (V x) := fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, hxV _⟩
-  rcases hK.elim_finite_subcover _ (fun x => @isOpen_interior X _ (V x)) this with ⟨t, ht⟩
-  refine'
-    ⟨_, t.isCompact_biUnion fun x _ => hVc x, fun x hx => _, Set.iUnion₂_subset fun i _ => hKV i⟩
-  rcases mem_iUnion₂.1 (ht hx) with ⟨y, hyt, hy⟩
-  exact interior_mono (subset_iUnion₂ y hyt) hy
+theorem exists_compact_between [LocallyCompactSpace X] {K U : Set X} (hK : IsCompact K)
+    (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U :=
+  let ⟨L, hKL, hL, hLU⟩ := exists_mem_nhdsSet_isCompact_mapsTo continuous_id hK hU h_KU
+  ⟨L, hL, subset_interior_iff_mem_nhdsSet.2 hKL, hLU⟩
 #align exists_compact_between exists_compact_between
 
 protected theorem ClosedEmbedding.locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y}

Mathlib/Topology/Connected/PathConnected.lean

@@ -215,7 +215,7 @@ 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 :=
-  continuous_eval'.comp <| (continuous_induced_dom (α := Path x y)).prod_map continuous_id
+  continuous_eval.comp <| (continuous_induced_dom (α := Path x y)).prod_map continuous_id
 #align path.continuous_eval Path.continuous_eval
 
 @[continuity]

Mathlib/Topology/ContinuousFunction/Algebra.lean

@@ -336,9 +336,9 @@ instance [LocallyCompactSpace α] [Mul β] [ContinuousMul β] : ContinuousMul C(
   ⟨by
     refine' continuous_of_continuous_uncurry _ _
     have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
-      continuous_eval'.comp (continuous_fst.prod_map continuous_id)
+      continuous_eval.comp (continuous_fst.prod_map continuous_id)
     have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
-      continuous_eval'.comp (continuous_snd.prod_map continuous_id)
+      continuous_eval.comp (continuous_snd.prod_map continuous_id)
     exact h1.mul h2⟩
 
 /-- Coercion to a function as a `MonoidHom`. Similar to `MonoidHom.coeFn`. -/
@@ -603,15 +603,15 @@ instance instSMul [SMul R M] [ContinuousConstSMul R M] : SMul R C(α, M) :=
 @[to_additive]
 instance [LocallyCompactSpace α] [SMul R M] [ContinuousConstSMul R M] :
     ContinuousConstSMul R C(α, M) :=
-  ⟨fun γ => continuous_of_continuous_uncurry _ (continuous_eval'.const_smul γ)⟩
+  ⟨fun γ => continuous_of_continuous_uncurry _ (continuous_eval.const_smul γ)⟩
 
 @[to_additive]
 instance [LocallyCompactSpace α] [TopologicalSpace R] [SMul R M] [ContinuousSMul R M] :
     ContinuousSMul R C(α, M) :=
   ⟨by
     refine' continuous_of_continuous_uncurry _ _
     have h : Continuous fun x : (R × C(α, M)) × α => x.fst.snd x.snd :=
-      continuous_eval'.comp (continuous_snd.prod_map continuous_id)
+      continuous_eval.comp (continuous_snd.prod_map continuous_id)
     exact (continuous_fst.comp continuous_fst).smul h⟩
 
 @[to_additive (attr := simp, norm_cast)]

Mathlib/Topology/ContinuousFunction/Compact.lean

@@ -159,12 +159,6 @@ end
 instance [CompleteSpace β] : CompleteSpace C(α, β) :=
   (isometryEquivBoundedOfCompact α β).completeSpace
 
-/-- See also `ContinuousMap.continuous_eval'`. -/
-@[continuity]
-theorem continuous_eval : Continuous fun p : C(α, β) × α => p.1 p.2 :=
-  continuous_eval.comp ((isometryEquivBoundedOfCompact α β).continuous.prod_map continuous_id)
-#align continuous_map.continuous_eval ContinuousMap.continuous_eval
-
 -- TODO at some point we will need lemmas characterising this norm!
 -- At the moment the only way to reason about it is to transfer `f : C(α,E)` back to `α →ᵇ E`.
 instance : Norm C(α, E) where norm x := dist x 0

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -214,7 +214,7 @@ def toLoop (i : N) (p : Ω^ N X x) : Ω (Ω^ { j // j ≠ i } X x) const
 theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
   Path.continuous_uncurry_iff.1 <|
     Continuous.subtype_mk
-      (ContinuousMap.continuous_eval'.comp <|
+      (ContinuousMap.continuous_eval.comp <|
         Continuous.prod_map
           (ContinuousMap.continuous_curry.comp <|
             (ContinuousMap.continuous_comp_left _).comp continuous_subtype_val)