chore(ContinuousMap/Defs): extract from Basic (#17265)

Move the definition of `ContinuousMap` to a new file
that doesn't depend on `Homeomorph`, `Separation` etc

Also use `X`/`Y` instead of `α`/`β` for type vars in the new file.

Mathlib.lean

@@ -4617,6 +4617,7 @@ import Mathlib.Topology.ContinuousMap.CocompactMap
 import Mathlib.Topology.ContinuousMap.Compact
 import Mathlib.Topology.ContinuousMap.CompactlySupported
 import Mathlib.Topology.ContinuousMap.ContinuousMapZero
+import Mathlib.Topology.ContinuousMap.Defs
 import Mathlib.Topology.ContinuousMap.Ideals
 import Mathlib.Topology.ContinuousMap.LocallyConstant
 import Mathlib.Topology.ContinuousMap.Ordered

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -334,9 +334,9 @@ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
     rw [Set.preimage_preimage]
     change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _
     -- Porting note: used to be `congr 3`
-    refine congr_arg (· ⁻¹' _) ?_
-    convert congr_arg (ContinuousMap.toFun (α := D.V ⟨j, k⟩) (β := D.glued) ·) ?_
-    refine congr_arg (PresheafedSpace.Hom.base (C := C) ·) ?_
+    suffices D.f j k ≫ D.ι j = colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k)) by
+      rw [this]
+      rfl
     exact colimit.w 𝖣.diagram.multispan (WalkingMultispan.Hom.fst (j, k))
   · exact D.opensImagePreimageMap i j U
 

Mathlib/Topology/Algebra/ContinuousAffineMap.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.LinearAlgebra.AffineSpace.AffineMap
-import Mathlib.Topology.ContinuousMap.Basic
 import Mathlib.Topology.Algebra.Module.Basic
 
 /-!

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -7,7 +7,6 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.UniformGroup
-import Mathlib.Topology.ContinuousMap.Basic
 import Mathlib.Topology.UniformSpace.UniformEmbedding
 import Mathlib.Algebra.Algebra.Defs
 import Mathlib.LinearAlgebra.Projection

Mathlib/Topology/Algebra/Monoid.lean

@@ -7,8 +7,8 @@ import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Order.Filter.Pointwise
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Topology.ContinuousMap.Basic
 import Mathlib.Algebra.Group.ULift
+import Mathlib.Topology.ContinuousMap.Defs
 
 /-!
 # Theory of topological monoids

Mathlib/Topology/Algebra/Star.lean

@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.Algebra.Star.Pi
 import Mathlib.Algebra.Star.Prod
 import Mathlib.Topology.Algebra.Constructions
-import Mathlib.Topology.ContinuousMap.Basic
+import Mathlib.Topology.ContinuousMap.Defs
 
 /-!
 # Continuity of `star`

Mathlib/Topology/Category/TopCat/Basic.lean

@@ -56,7 +56,7 @@ instance topologicalSpaceUnbundled (X : TopCat) : TopologicalSpace X :=
 instance instFunLike (X Y : TopCat) : FunLike (X ⟶ Y) X Y :=
   inferInstanceAs <| FunLike C(X, Y) X Y
 
-instance instMonoidHomClass (X Y : TopCat) : ContinuousMapClass (X ⟶ Y) X Y :=
+instance instContinuousMapClass (X Y : TopCat) : ContinuousMapClass (X ⟶ Y) X Y :=
   inferInstanceAs <| ContinuousMapClass C(X, Y) X Y
 
 -- Porting note (#10618): simp can prove this; removed simp

Mathlib/Topology/ContinuousMap/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 -/
 import Mathlib.Data.Set.UnionLift
+import Mathlib.Topology.ContinuousMap.Defs
 import Mathlib.Topology.Homeomorph
 
 /-!
@@ -19,37 +20,6 @@ be satisfied by itself and all stricter types.
 open Function
 open scoped Topology
 
-/-- The type of continuous maps from `α` to `β`.
-
-When possible, instead of parametrizing results over `(f : C(α, β))`,
-you should parametrize over `{F : Type*} [ContinuousMapClass F α β] (f : F)`.
-
-When you extend this structure, make sure to extend `ContinuousMapClass`. -/
-structure ContinuousMap (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] where
-  /-- The function `α → β` -/
-  protected toFun : α → β
-  /-- Proposition that `toFun` is continuous -/
-  protected continuous_toFun : Continuous toFun := by continuity
-
-/-- The type of continuous maps from `α` to `β`. -/
-notation "C(" α ", " β ")" => ContinuousMap α β
-
-section
-
-/-- `ContinuousMapClass F α β` states that `F` is a type of continuous maps.
-
-You should extend this class when you extend `ContinuousMap`. -/
-class ContinuousMapClass (F : Type*) (α β : outParam Type*)
-    [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] : Prop where
-  /-- Continuity -/
-  map_continuous (f : F) : Continuous f
-
-end
-
-export ContinuousMapClass (map_continuous)
-
-attribute [continuity, fun_prop] map_continuous
-
 section ContinuousMapClass
 
 variable {F α β : Type*} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β]
@@ -61,11 +31,6 @@ theorem map_continuousAt (f : F) (a : α) : ContinuousAt f a :=
 theorem map_continuousWithinAt (f : F) (s : Set α) (a : α) : ContinuousWithinAt f s a :=
   (map_continuous f).continuousWithinAt
 
-/-- Coerce a bundled morphism with a `ContinuousMapClass` instance to a `ContinuousMap`. -/
-@[coe] def toContinuousMap (f : F) : C(α, β) := ⟨f, map_continuous f⟩
-
-instance : CoeTC F C(α, β) := ⟨toContinuousMap⟩
-
 end ContinuousMapClass
 
 /-! ### Continuous maps -/
@@ -76,75 +41,11 @@ namespace ContinuousMap
 variable {α β γ δ : Type*} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
   [TopologicalSpace δ]
 
-instance funLike : FunLike C(α, β) α β where
-  coe := ContinuousMap.toFun
-  coe_injective' f g h := by cases f; cases g; congr
-
-instance toContinuousMapClass : ContinuousMapClass C(α, β) α β where
-  map_continuous := ContinuousMap.continuous_toFun
-
-@[simp]
-theorem toFun_eq_coe {f : C(α, β)} : f.toFun = (f : α → β) :=
-  rfl
-
-instance : CanLift (α → β) C(α, β) DFunLike.coe Continuous := ⟨fun f hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
-
-/-- See note [custom simps projection]. -/
-def Simps.apply (f : C(α, β)) : α → β := f
-
--- this must come after the coe_to_fun definition
-initialize_simps_projections ContinuousMap (toFun → apply)
-
-@[simp] -- Porting note: removed `norm_cast` attribute
-protected theorem coe_coe {F : Type*} [FunLike F α β] [ContinuousMapClass F α β] (f : F) :
-    ⇑(f : C(α, β)) = f :=
-  rfl
-
-@[ext]
-theorem ext {f g : C(α, β)} (h : ∀ a, f a = g a) : f = g :=
-  DFunLike.ext _ _ h
-
-/-- Copy of a `ContinuousMap` with a new `toFun` equal to the old one. Useful to fix definitional
-equalities. -/
-protected def copy (f : C(α, β)) (f' : α → β) (h : f' = f) : C(α, β) where
-  toFun := f'
-  continuous_toFun := h.symm ▸ f.continuous_toFun
-
-@[simp]
-theorem coe_copy (f : C(α, β)) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
-  rfl
-
-theorem copy_eq (f : C(α, β)) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
-  DFunLike.ext' h
-
 variable {f g : C(α, β)}
 
-/-- Deprecated. Use `map_continuous` instead. -/
-protected theorem continuous (f : C(α, β)) : Continuous f :=
-  f.continuous_toFun
-
-@[continuity]
-theorem continuous_set_coe (s : Set C(α, β)) (f : s) : Continuous (f : α → β) :=
-  f.1.continuous
-
 /-- Deprecated. Use `map_continuousAt` instead. -/
 protected theorem continuousAt (f : C(α, β)) (x : α) : ContinuousAt f x :=
-  f.continuous.continuousAt
-
-/-- Deprecated. Use `DFunLike.congr_fun` instead. -/
-protected theorem congr_fun {f g : C(α, β)} (H : f = g) (x : α) : f x = g x :=
-  H ▸ rfl
-
-/-- Deprecated. Use `DFunLike.congr_arg` instead. -/
-protected theorem congr_arg (f : C(α, β)) {x y : α} (h : x = y) : f x = f y :=
-  h ▸ rfl
-
-theorem coe_injective : @Function.Injective C(α, β) (α → β) (↑) := fun f g h => by
-  cases f; cases g; congr
-
-@[simp]
-theorem coe_mk (f : α → β) (h : Continuous f) : ⇑(⟨f, h⟩ : C(α, β)) = f :=
-  rfl
+  map_continuousAt f x
 
 theorem map_specializes (f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y :=
   h.map f.2
@@ -378,13 +279,14 @@ theorem restrict_apply_mk (f : C(α, β)) (s : Set α) (x : α) (hx : x ∈ s) :
 
 theorem injective_restrict [T2Space β] {s : Set α} (hs : Dense s) :
     Injective (restrict s : C(α, β) → C(s, β)) := fun f g h ↦
-  DFunLike.ext' <| f.continuous.ext_on hs g.continuous <| Set.restrict_eq_restrict_iff.1 <|
-    congr_arg DFunLike.coe h
+  DFunLike.ext' <| (map_continuous f).ext_on hs (map_continuous g) <|
+    Set.restrict_eq_restrict_iff.1 <| congr_arg DFunLike.coe h
 
 /-- The restriction of a continuous map to the preimage of a set. -/
 @[simps]
 def restrictPreimage (f : C(α, β)) (s : Set β) : C(f ⁻¹' s, s) :=
-  ⟨s.restrictPreimage f, continuous_iff_continuousAt.mpr fun _ => f.2.continuousAt.restrictPreimage⟩
+  ⟨s.restrictPreimage f, continuous_iff_continuousAt.mpr fun _ ↦
+    (map_continuousAt f _).restrictPreimage⟩
 
 end Restrict
 
@@ -402,8 +304,8 @@ noncomputable def liftCover : C(α, β) :=
     Set.iUnion_eq_univ_iff.2 fun x ↦ (hS x).imp fun _ ↦ mem_of_mem_nhds
   mk (Set.liftCover S (fun i ↦ φ i) hφ H) <| continuous_of_cover_nhds hS fun i ↦ by
     rw [continuousOn_iff_continuous_restrict]
-    simpa (config := { unfoldPartialApp := true }) only [Set.restrict, Set.liftCover_coe] using
-      (φ i).continuous
+    simpa (config := { unfoldPartialApp := true }) only [Set.restrict, Set.liftCover_coe]
+      using map_continuous (φ i)
 
 variable {S φ hφ hS}
 
@@ -461,8 +363,8 @@ variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalS
 def Function.RightInverse.homeomorph {f' : C(Y, X)} (hf : Function.RightInverse f' f) :
     Quotient (Setoid.ker f) ≃ₜ Y where
   toEquiv := Setoid.quotientKerEquivOfRightInverse _ _ hf
-  continuous_toFun := quotientMap_quot_mk.continuous_iff.mpr f.continuous
-  continuous_invFun := continuous_quotient_mk'.comp f'.continuous
+  continuous_toFun := quotientMap_quot_mk.continuous_iff.mpr (map_continuous f)
+  continuous_invFun := continuous_quotient_mk'.comp (map_continuous f')
 
 namespace QuotientMap
 

Mathlib/Topology/ContinuousMap/CompactlySupported.lean

@@ -119,7 +119,6 @@ theorem eq_of_empty [IsEmpty α] (f g : C_c(α, β)) : f = g :=
 def ContinuousMap.liftCompactlySupported [CompactSpace α] : C(α, β) ≃ C_c(α, β) where
   toFun f :=
     { toFun := f
-      continuous_toFun := f.continuous
       hasCompactSupport' := HasCompactSupport.of_compactSpace f }
   invFun f := f
   left_inv _ := rfl
@@ -168,7 +167,7 @@ theorem mul_apply [MulZeroClass β] [ContinuousMul β] (f g : C_c(α, β)) : (f
 instance [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β]
     {F : Type*} [FunLike F α γ] [ContinuousMapClass F α γ] : SMul F C_c(α, β) where
   smul f g :=
-    ⟨⟨fun x ↦ f x • g x, (map_continuous f).smul g.continuous⟩, g.hasCompactSupport'.smul_left⟩
+    ⟨⟨fun x ↦ f x • g x, (map_continuous f).smul (map_continuous g)⟩, g.hasCompactSupport.smul_left⟩
 
 @[simp]
 theorem coe_smulc [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β]
@@ -209,7 +208,7 @@ def coeFnMonoidHom [AddMonoid β] [ContinuousAdd β] : C_c(α, β) →+ α → 
 
 instance [Zero β] {R : Type*} [SMulZeroClass R β] [ContinuousConstSMul R β] :
     SMul R C_c(α, β) :=
-  ⟨fun r f => ⟨⟨r • ⇑f, Continuous.const_smul f.continuous r⟩, HasCompactSupport.smul_left f.2⟩⟩
+  ⟨fun r f => ⟨⟨r • ⇑f, (map_continuous f).const_smul r⟩, HasCompactSupport.smul_left f.2⟩⟩
 
 @[simp, norm_cast]
 theorem coe_smul [Zero β] {R : Type*} [SMulZeroClass R β] [ContinuousConstSMul R β] (r : R)