chore(ContinuousMap): move compRight* (#17935)

Also drop some unneeded assumptions and rename/deprecate some lemmas.

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

@@ -83,10 +83,7 @@ lemma isClosedEmbedding_cfcₙAux : IsClosedEmbedding (cfcₙAux hp₁ a ha) :=
   refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
     ContinuousMapZero.isClosedEmbedding_toContinuousMap
   let e : C(σₙ 𝕜 a, 𝕜) ≃ₜ C(σ 𝕜 (a : A⁺¹), 𝕜) :=
-    { (Homeomorph.compStarAlgEquiv' 𝕜 𝕜 <| .setCongr <|
-        (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm) with
-      continuous_toFun := ContinuousMap.continuous_comp_left _
-      continuous_invFun := ContinuousMap.continuous_comp_left _ }
+    (Homeomorph.setCongr (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a)).arrowCongr (.refl _)
   exact e.isClosedEmbedding
 
 @[deprecated (since := "2024-10-20")]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -178,7 +178,7 @@ theorem cfcₙHom_comp [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : C(
   suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
   · refine (cfcₙHom_isClosedEmbedding ha).continuous.comp <| continuous_induced_rng.mpr ?_
-    exact f'.toContinuousMap.continuous_comp_left.comp continuous_induced_dom
+    exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom
   · simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk',
       NonUnitalAlgHom.coe_mk]
     congr

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

@@ -56,7 +56,7 @@ namespace ContinuousMap
 noncomputable def toNNReal (f : C(X, ℝ)) : C(X, ℝ≥0) := .realToNNReal |>.comp f
 
 @[fun_prop]
-lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_comp _
+lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_postcomp _
 
 @[simp]
 lemma toNNReal_apply (f : C(X, ℝ)) (x : X) : f.toNNReal x = (f x).toNNReal := rfl
@@ -187,7 +187,7 @@ instance NNReal.instUniqueContinuousFunctionalCalculus [UniqueContinuousFunction
         Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
-        ContinuousMap.continuous_comp_left _, ?_⟩
+        ContinuousMap.continuous_precomp _, ?_⟩
       exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ
@@ -249,7 +249,7 @@ lemma toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal (
 lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := by
   rw [continuous_induced_rng]
   convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
-  exact ContinuousMap.continuous_comp _ |>.comp continuous_induced_dom
+  exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom
 
 lemma toContinuousMapHom_toNNReal (f : C(X, ℝ)₀) :
     (toContinuousMapHom (X := X) (R := ℝ) f).toNNReal =
@@ -401,7 +401,7 @@ instance NNReal.instUniqueNonUnitalContinuousFunctionalCalculus
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
       · rw [continuous_induced_rng]
-        exact ContinuousMap.continuous_comp_left _ |>.comp continuous_induced_dom
+        exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom
       · exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id h0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -271,7 +271,7 @@ theorem cfcHom_comp [UniqueContinuousFunctionalCalculus R A] (f : C(spectrum R a
     (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f'
   suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_
-  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_comp_left
+  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_precomp
   · simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]
     congr
     ext x

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -302,13 +302,13 @@ theorem continuous_comp [LocallyCompactSpace B] :
 theorem continuous_comp_left (f : ContinuousMonoidHom A B) :
     Continuous fun g : ContinuousMonoidHom B C => g.comp f :=
   (inducing_toContinuousMap A C).continuous_iff.2 <|
-    f.toContinuousMap.continuous_comp_left.comp (inducing_toContinuousMap B C).continuous
+    f.toContinuousMap.continuous_precomp.comp (inducing_toContinuousMap B C).continuous
 
 @[to_additive]
 theorem continuous_comp_right (f : ContinuousMonoidHom B C) :
     Continuous fun g : ContinuousMonoidHom A B => f.comp g :=
   (inducing_toContinuousMap A C).continuous_iff.2 <|
-    f.toContinuousMap.continuous_comp.comp (inducing_toContinuousMap A B).continuous
+    f.toContinuousMap.continuous_postcomp.comp (inducing_toContinuousMap A B).continuous
 
 variable (E)
 

Mathlib/Topology/CompactOpen.lean

@@ -78,27 +78,45 @@ lemma continuous_compactOpen {f : X → C(Y, Z)} :
 section Functorial
 
 /-- `C(X, ·)` is a functor. -/
-theorem continuous_comp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
+theorem continuous_postcomp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
   continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2)
 
+@[deprecated (since := "2024-10-19")] alias continuous_comp := continuous_postcomp
+
 /-- If `g : C(Y, Z)` is a topology inducing map,
 then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is a topology inducing map too. -/
-theorem inducing_comp (g : C(Y, Z)) (hg : Inducing g) : Inducing (g.comp : C(X, Y) → C(X, Z)) where
+theorem inducing_postcomp (g : C(Y, Z)) (hg : Inducing g) :
+    Inducing (g.comp : C(X, Y) → C(X, Z)) where
   induced := by
     simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
       image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]
 
+@[deprecated (since := "2024-10-19")] alias inducing_comp := inducing_postcomp
+
 /-- If `g : C(Y, Z)` is a topological embedding,
 then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too. -/
-theorem embedding_comp (g : C(Y, Z)) (hg : Embedding g) : Embedding (g.comp : C(X, Y) → C(X, Z)) :=
-  ⟨inducing_comp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩
+theorem embedding_postcomp (g : C(Y, Z)) (hg : Embedding g) :
+    Embedding (g.comp : C(X, Y) → C(X, Z)) :=
+  ⟨inducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩
+
+@[deprecated (since := "2024-10-19")] alias embedding_comp := embedding_postcomp
 
 /-- `C(·, Z)` is a functor. -/
-@[fun_prop]
-theorem continuous_comp_left (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
+@[continuity, fun_prop]
+theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
   continuous_compactOpen.2 fun K hK U hU ↦ by
     simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU
 
+@[deprecated (since := "2024-10-19")] alias continuous_comp_left := continuous_precomp
+
+variable (Z) in
+/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
+-/
+@[simps apply]
+def compRightContinuousMap (f : C(X, Y)) :
+    C(C(Y, Z), C(X, Z)) where
+  toFun g := g.comp f
+
 /-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism
 `C(X, Y) ≃ₜ C(Z, T)`. -/
 protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
@@ -107,8 +125,16 @@ protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
   invFun f := .comp ψ.symm <| f.comp φ
   left_inv f := ext fun _ ↦ ψ.left_inv (f _) |>.trans <| congrArg f <| φ.left_inv _
   right_inv f := ext fun _ ↦ ψ.right_inv (f _) |>.trans <| congrArg f <| φ.right_inv _
-  continuous_toFun := continuous_comp _ |>.comp <| continuous_comp_left _
-  continuous_invFun := continuous_comp _ |>.comp <| continuous_comp_left _
+  continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _
+  continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _
+
+variable (Z) in
+/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.
+-/
+@[deprecated Homeomorph.arrowCongr (since := "2024-10-19")]
+def compRightHomeomorph (f : X ≃ₜ Y) :
+    C(Y, Z) ≃ₜ C(X, Z) :=
+  .arrowCongr f.symm (.refl _)
 
 variable [LocallyCompactPair Y Z]
 
@@ -234,7 +260,7 @@ section InfInduced
 /-- For any subset `s` of `X`, the restriction of continuous functions to `s` is continuous
 as a function from `C(X, Y)` to `C(s, Y)` with their respective compact-open topologies. -/
 theorem continuous_restrict (s : Set X) : Continuous fun F : C(X, Y) => F.restrict s :=
-  continuous_comp_left <| restrict s <| .id X
+  continuous_precomp <| restrict s <| .id X
 
 theorem compactOpen_le_induced (s : Set X) :
     (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤
@@ -340,7 +366,7 @@ section Curry
     compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
 def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where
   toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩
-  continuous_toFun := (continuous_comp f).comp continuous_coev
+  continuous_toFun := (continuous_postcomp f).comp continuous_coev
 
 @[simp]
 theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) :=

Mathlib/Topology/ContinuousMap/Algebra.lean

@@ -697,6 +697,10 @@ def ContinuousMap.compRightAlgHom {α β : Type*} [TopologicalSpace α] [Topolog
   map_mul' _ _ := ext fun _ ↦ rfl
   commutes' _ := ext fun _ ↦ rfl
 
+theorem ContinuousMap.compRightAlgHom_continuous {α β : Type*} [TopologicalSpace α]
+    [TopologicalSpace β] (f : C(α, β)) : Continuous (compRightAlgHom R A f) :=
+  continuous_precomp f
+
 variable {A}
 
 /-- Coercion to a function as an `AlgHom`. -/

Mathlib/Topology/ContinuousMap/Compact.lean

@@ -417,57 +417,6 @@ end CompLeft
 
 namespace ContinuousMap
 
-/-!
-We now setup variations on `compRight* f`, where `f : C(X, Y)`
-(that is, precomposition by a continuous map),
-as a morphism `C(Y, T) → C(X, T)`, respecting various types of structure.
-
-In particular:
-* `compRightContinuousMap`, the bundled continuous map (for this we need `X Y` compact).
-* `compRightHomeomorph`, when we precompose by a homeomorphism.
-* `compRightAlgHom`, when `T = R` is a topological ring.
--/
-
-
-section CompRight
-
-/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
--/
-def compRightContinuousMap {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X]
-    [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y)) :
-    C(C(Y, T), C(X, T)) where
-  toFun g := g.comp f
-  continuous_toFun := by
-    refine Metric.continuous_iff.mpr ?_
-    intro g ε ε_pos
-    refine ⟨ε, ε_pos, fun g' h => ?_⟩
-    rw [ContinuousMap.dist_lt_iff ε_pos] at h ⊢
-    exact fun x => h (f x)
-
-@[simp]
-theorem compRightContinuousMap_apply {X Y : Type*} (T : Type*) [TopologicalSpace X]
-    [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y))
-    (g : C(Y, T)) : (compRightContinuousMap T f) g = g.comp f :=
-  rfl
-
-/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.
--/
-def compRightHomeomorph {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X]
-    [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : X ≃ₜ Y) :
-    C(Y, T) ≃ₜ C(X, T) where
-  toFun := compRightContinuousMap T f
-  invFun := compRightContinuousMap T f.symm
-  left_inv g := ext fun _ => congr_arg g (f.apply_symm_apply _)
-  right_inv g := ext fun _ => congr_arg g (f.symm_apply_apply _)
-
-theorem compRightAlgHom_continuous {X Y : Type*} (R A : Type*) [TopologicalSpace X]
-    [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [CommSemiring R] [Semiring A]
-    [PseudoMetricSpace A] [TopologicalSemiring A] [Algebra R A] (f : C(X, Y)) :
-    Continuous (compRightAlgHom R A f) :=
-  map_continuous (compRightContinuousMap A f)
-
-end CompRight
-
 section LocalNormalConvergence
 
 /-! ### Local normal convergence
@@ -476,7 +425,6 @@ A sum of continuous functions (on a locally compact space) is "locally normally
 sum of its sup-norms on any compact subset is summable. This implies convergence in the topology
 of `C(X, E)` (i.e. locally uniform convergence). -/
 
-
 open TopologicalSpace
 
 variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X]

Mathlib/Topology/ContinuousMap/Sigma.lean

@@ -44,7 +44,7 @@ namespace ContinuousMap
 theorem embedding_sigmaMk_comp [Nonempty X] :
     Embedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where
   toInducing := inducing_sigma.2
-    ⟨fun i ↦ (sigmaMk i).inducing_comp embedding_sigmaMk.toInducing, fun i ↦
+    ⟨fun i ↦ (sigmaMk i).inducing_postcomp embedding_sigmaMk.toInducing, fun i ↦
       let ⟨x⟩ := ‹Nonempty X›
       ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩
   inj := by

Mathlib/Topology/ContinuousMap/Weierstrass.lean

@@ -58,7 +58,7 @@ theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
       compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm
     -- This operation is itself a homeomorphism
     -- (with respect to the norm topologies on continuous functions).
-    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm
+    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)
     have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
     -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`,
     have p := polynomialFunctions_closure_eq_top'

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -192,7 +192,7 @@ theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
       (continuous_eval.comp <|
         Continuous.prodMap
           (ContinuousMap.continuous_curry.comp <|
-            (ContinuousMap.continuous_comp_left _).comp continuous_subtype_val)
+            (ContinuousMap.continuous_precomp _).comp continuous_subtype_val)
           continuous_id)
       _
 
@@ -211,9 +211,9 @@ def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x :=
     · exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩⟩
 
 theorem continuous_fromLoop (i : N) : Continuous (@fromLoop N X _ x _ i) :=
-  ((ContinuousMap.continuous_comp_left _).comp <|
+  ((ContinuousMap.continuous_precomp _).comp <|
         ContinuousMap.continuous_uncurry.comp <|
-          (ContinuousMap.continuous_comp _).comp continuous_induced_dom).subtype_mk
+          (ContinuousMap.continuous_postcomp _).comp continuous_induced_dom).subtype_mk
     _
 
 theorem to_from (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : toLoop i (fromLoop i p) = p := by
@@ -244,7 +244,7 @@ theorem fromLoop_apply (i : N) {p : Ω (Ω^ { j // j ≠ i } X x) const} {t : I^
 /-- Composition with `Cube.insertAt` as a continuous map. -/
 abbrev cCompInsert (i : N) : C(C(I^N, X), C(I × I^{ j // j ≠ i }, X)) :=
   ⟨fun f => f.comp (Cube.insertAt i),
-    (toContinuousMap <| Cube.insertAt i).continuous_comp_left⟩
+    (toContinuousMap <| Cube.insertAt i).continuous_precomp⟩
 
 /-- A homotopy between `n+1`-dimensional loops `p` and `q` constant on the boundary
   seen as a homotopy between two paths in the space of `n`-dimensional paths. -/