diff --git a/Mathlib/Algebra/Category/Grp/AB.lean b/Mathlib/Algebra/Category/Grp/AB.lean
index 640bf9e62beb76..8396f882c110ec 100644
--- a/Mathlib/Algebra/Category/Grp/AB.lean
+++ b/Mathlib/Algebra/Category/Grp/AB.lean
@@ -72,7 +72,7 @@ instance : HasExactLimitsOfShape (Discrete J) (AddCommGrpCat.{u}) := by
         (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
       let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
         (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
-      have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
+      have : Function.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
         simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
           IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
           Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
@@ -83,7 +83,7 @@ instance : HasExactLimitsOfShape (Discrete J) (AddCommGrpCat.{u}) := by
         ext g j
         change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
         simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π, Fan.mk_pt,
-          Fan.mk_π_app, Pi.map_apply]
+          Fan.mk_π_app, Function.map_apply]
         change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
         simp
       suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean
index 77be7fd2c8ebe0..3168b7d3efebdb 100644
--- a/Mathlib/Algebra/Notation/Pi/Defs.lean
+++ b/Mathlib/Algebra/Notation/Pi/Defs.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Notation.Defs
 public import Mathlib.Tactic.Push.Attr
 public import Mathlib.Logic.Function.Defs
-public import Batteries.Tactic.Alias
 
 /-!
 # Notation for algebraic operators on pi types
diff --git a/Mathlib/Algebra/Order/Antidiag/Nat.lean b/Mathlib/Algebra/Order/Antidiag/Nat.lean
index 1da55e696c5940..7403450bdf4420 100644
--- a/Mathlib/Algebra/Order/Antidiag/Nat.lean
+++ b/Mathlib/Algebra/Order/Antidiag/Nat.lean
@@ -69,7 +69,7 @@ theorem mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} :
       Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
       Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
       toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
-      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
+      Equiv.piCongrRight_apply, Function.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
       PNat.coe_prod]
     constructor
     · rintro ⟨a, ha_mem, rfl⟩
diff --git a/Mathlib/Algebra/Regular/Pi.lean b/Mathlib/Algebra/Regular/Pi.lean
index 1baaa86a404621..66d927c4b84ab7 100644
--- a/Mathlib/Algebra/Regular/Pi.lean
+++ b/Mathlib/Algebra/Regular/Pi.lean
@@ -22,11 +22,11 @@ variable [∀ i, Mul (R i)]
 
 @[to_additive (attr := simp)]
 theorem isLeftRegular_iff {a : ∀ i, R i} : IsLeftRegular a ↔ ∀ i, IsLeftRegular (a i) :=
-  have (i : _) : Nonempty (R i) := ⟨a i⟩; Pi.map_injective
+  have (i : _) : Nonempty (R i) := ⟨a i⟩; Function.map_injective
 
 @[to_additive (attr := simp)]
 theorem isRightRegular_iff {a : ∀ i, R i} : IsRightRegular a ↔ ∀ i, IsRightRegular (a i) :=
-  have (i : _) : Nonempty (R i) := ⟨a i⟩; .symm <| Pi.map_injective.symm
+  have (i : _) : Nonempty (R i) := ⟨a i⟩; .symm <| Function.map_injective.symm
 
 @[to_additive (attr := simp)]
 theorem isRegular_iff {a : ∀ i, R i} : IsRegular a ↔ ∀ i, IsRegular (a i) := by
@@ -37,6 +37,6 @@ end
 @[simp]
 theorem isSMulRegular_iff [∀ i, SMul α (R i)] {r : α} [∀ i, Nonempty (R i)] :
     IsSMulRegular (∀ i, R i) r ↔ ∀ i, IsSMulRegular (R i) r :=
-  Pi.map_injective
+  Function.map_injective
 
 end Pi
diff --git a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
index a4e67bc0f020af..ab702f0253ec75 100644
--- a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
@@ -39,9 +39,9 @@ open EuclideanSpace in
 /-- The comultiplication on `n → 𝕜` corresponds to the Euclidean space adjoint of the
 multiplication map. -/
 theorem Pi.comul_eq_adjoint {n : Type*} [Fintype n] [DecidableEq n] :
-    comul = map (equiv n 𝕜).toLinearMap (equiv n 𝕜).toLinearMap ∘ₗ
+    comul = TensorProduct.map (equiv n 𝕜).toLinearMap (equiv n 𝕜).toLinearMap ∘ₗ
       ((equiv n 𝕜).symm.toLinearMap ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ
-        map (equiv n 𝕜).toLinearMap (equiv n 𝕜).toLinearMap).adjoint ∘ₗ
+        TensorProduct.map (equiv n 𝕜).toLinearMap (equiv n 𝕜).toLinearMap).adjoint ∘ₗ
       (equiv n 𝕜).symm.toLinearMap := by
   ext
   simp only [comp_apply, ← toLinearMap_congr, LinearEquiv.coe_coe, ← LinearEquiv.symm_apply_eq]
diff --git a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
index 3ca87f8a6ffbab..c2313134cdb932 100644
--- a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
+++ b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
@@ -256,7 +256,7 @@ theorem det_fderivPiPolarCoordSymm (p : ι → ℝ × ℝ) :
   simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]
 
 theorem pi_polarCoord_symm_target_ae_eq_univ :
-    (Pi.map (fun _ : ι ↦ polarCoord.symm) '' Set.univ.pi fun _ ↦ polarCoord.target)
+    (Function.map (fun _ : ι ↦ polarCoord.symm) '' Set.univ.pi fun _ ↦ polarCoord.target)
         =ᵐ[volume] Set.univ := by
   rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
   exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ
diff --git a/Mathlib/Condensed/Discrete/LocallyConstant.lean b/Mathlib/Condensed/Discrete/LocallyConstant.lean
index 6ec60e11b2fc81..4201e0978c7eff 100644
--- a/Mathlib/Condensed/Discrete/LocallyConstant.lean
+++ b/Mathlib/Condensed/Discrete/LocallyConstant.lean
@@ -276,7 +276,7 @@ noncomputable def counit [HasExplicitFiniteCoproducts.{u} P] : haveI := CompHaus
     apply presheaf_ext (f.comap (sigmaIncl _ _).hom.hom)
     intro b
     simp only [counitAppAppImage, ← Functor.map_comp_apply, ← op_comp,
-      map_apply, IsTerminal.comp_from, ← map_preimage_eq_image_map]
+      LocallyConstant.map_apply, IsTerminal.comp_from, ← map_preimage_eq_image_map]
     change (_ ≫ Y.obj.map _) _ = (_ ≫ Y.obj.map _) _
     simp only [← g.hom.naturality]
     rw [show sigmaIncl (f.comap (sigmaIncl (f.map _) a).hom.hom) b ≫ sigmaIncl (f.map _) a =
diff --git a/Mathlib/Control/Bifunctor.lean b/Mathlib/Control/Bifunctor.lean
index b9cd394f8d7cf6..e9d5ba21dd0ce3 100644
--- a/Mathlib/Control/Bifunctor.lean
+++ b/Mathlib/Control/Bifunctor.lean
@@ -29,8 +29,6 @@ public section
 
 universe u₀ u₁ u₂ v₀ v₁ v₂
 
-open Function
-
 /-- Lawless bifunctor. This typeclass only holds the data for the bimap. -/
 class Bifunctor (F : Type u₀ → Type u₁ → Type u₂) where
   bimap : ∀ {α α' β β'}, (α → α') → (β → β') → F α β → F α' β'
@@ -142,7 +140,7 @@ instance Function.bicompl.bifunctor : Bifunctor (bicompl F G H) where
 
 instance Function.bicompl.lawfulBifunctor [LawfulFunctor G] [LawfulFunctor H] [LawfulBifunctor F] :
     LawfulBifunctor (bicompl F G H) := by
-  constructor <;> intros <;> simp [bimap, map_id, map_comp_map, functor_norm]
+  constructor <;> intros <;> simp [bimap, Functor.map_id, Functor.map_comp_map, functor_norm]
 
 end Bicompl
 
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
index 2a9df103936de6..ddef925d93e988 100644
--- a/Mathlib/Data/Finset/Powerset.lean
+++ b/Mathlib/Data/Finset/Powerset.lean
@@ -242,7 +242,7 @@ lemma powersetCard_empty_subsingleton (n : ℕ) :
 @[simp]
 theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
     (s.powersetCard i).val.map Finset.val = s.1.powersetCard i := by
-  simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']
+  simp [Finset.powersetCard, map_pmap, pmap_eq_map, Multiset.map_id']
 
 theorem powersetCard_one (s : Finset α) :
     s.powersetCard 1 = s.map ⟨_, Finset.singleton_injective⟩ :=
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
index afaeaafe82632a..b03e81b0776b15 100644
--- a/Mathlib/Data/Prod/Basic.lean
+++ b/Mathlib/Data/Prod/Basic.lean
@@ -231,7 +231,7 @@ theorem Bijective.prodMap (hf : Bijective f) (hg : Bijective g) : Bijective (map
 
 theorem LeftInverse.prodMap (hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) :
     LeftInverse (map f₁ g₁) (map f₂ g₂) :=
-  fun a ↦ by rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
+  fun a ↦ by rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, Prod.map_id, id]
 
 theorem RightInverse.prodMap :
     RightInverse f₁ f₂ → RightInverse g₁ g₂ → RightInverse (map f₁ g₁) (map f₂ g₂) :=
diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 161b9cca4c1660..cead5847f08fb8 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -789,15 +789,15 @@ theorem eval_image_univ_pi (ht : (pi univ t).Nonempty) :
 
 theorem piMap_mapsTo_pi {I : Set ι} {f : ∀ i, α i → β i} {s : ∀ i, Set (α i)} {t : ∀ i, Set (β i)}
     (h : ∀ i ∈ I, MapsTo (f i) (s i) (t i)) :
-    MapsTo (Pi.map f) (I.pi s) (I.pi t) :=
+    MapsTo (Function.map f) (I.pi s) (I.pi t) :=
   fun _x hx i hi => h i hi (hx i hi)
 
 theorem piMap_image_pi_subset {f : ∀ i, α i → β i} (t : ∀ i, Set (α i)) :
-    Pi.map f '' s.pi t ⊆ s.pi fun i ↦ f i '' t i :=
+    Function.map f '' s.pi t ⊆ s.pi fun i ↦ f i '' t i :=
   image_subset_iff.2 <| piMap_mapsTo_pi fun _ _ => mapsTo_image _ _
 
 theorem piMap_image_pi {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective (f i)) (t : ∀ i, Set (α i)) :
-    Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i := by
+    Function.map f '' s.pi t = s.pi fun i ↦ f i '' t i := by
   refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_
   have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
     if hi : i ∈ s then
@@ -808,11 +808,12 @@ theorem piMap_image_pi {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective
   exact ⟨a, hat, funext hab⟩
 
 theorem piMap_image_univ_pi (f : ∀ i, α i → β i) (t : ∀ i, Set (α i)) :
-    Pi.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i :=
+    Function.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i :=
   piMap_image_pi (by simp) t
 
 @[simp]
-theorem range_piMap (f : ∀ i, α i → β i) : range (Pi.map f) = pi univ fun i ↦ range (f i) := by
+theorem range_piMap (f : ∀ i, α i → β i) : range (Function.map f) =
+    pi univ fun i ↦ range (f i) := by
   simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]
 
 theorem subset_pi_iff {s'} : s' ⊆ pi s t ↔ ∀ i ∈ s, s' ⊆ (· i) ⁻¹' t i := by
diff --git a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
index 9397ca23a5b51e..21e65fd1c48201 100644
--- a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
+++ b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
@@ -73,7 +73,7 @@ theorem of_isEmpty [IsEmpty β] (f : α → β) (μa : Measure α) (μb : Measur
 theorem symm (e : α ≃ᵐ β) {μa : Measure α} {μb : Measure β} (h : MeasurePreserving e μa μb) :
     MeasurePreserving e.symm μb μa :=
   ⟨e.symm.measurable, by
-    rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩
+    rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, Measure.map_id]⟩
 
 theorem restrict_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β}
     (hs : MeasurableSet s) : MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
diff --git a/Mathlib/Dynamics/PeriodicPts/Defs.lean b/Mathlib/Dynamics/PeriodicPts/Defs.lean
index 53245e2d1fc261..89c08fd0880093 100644
--- a/Mathlib/Dynamics/PeriodicPts/Defs.lean
+++ b/Mathlib/Dynamics/PeriodicPts/Defs.lean
@@ -522,18 +522,18 @@ section Pi
 variable {ι : Type*} {α : ι → Type*} {f : ∀ i, α i → α i} {x : ∀ i, α i} {n : ℕ}
 
 @[simp]
-theorem isFixedPt_piMap : IsFixedPt (Pi.map f) x ↔ ∀ i, IsFixedPt (f i) (x i) :=
+theorem isFixedPt_piMap : IsFixedPt (Function.map f) x ↔ ∀ i, IsFixedPt (f i) (x i) :=
   funext_iff
 
-theorem IsFixedPt.piMap (h : ∀ i, IsFixedPt (f i) (x i)) : IsFixedPt (Pi.map f) x :=
+theorem IsFixedPt.piMap (h : ∀ i, IsFixedPt (f i) (x i)) : IsFixedPt (Function.map f) x :=
   isFixedPt_piMap.mpr h
 
 @[simp]
-theorem isPeriodicPt_piMap : IsPeriodicPt (Pi.map f) n x ↔ ∀ i, IsPeriodicPt (f i) n (x i) := by
-  simp [IsPeriodicPt]
+theorem isPeriodicPt_piMap : IsPeriodicPt (Function.map f) n x ↔
+    ∀ i, IsPeriodicPt (f i) n (x i) := by simp [IsPeriodicPt]
 
-theorem IsPeriodicPt.piMap (h : ∀ i, IsPeriodicPt (f i) n (x i)) : IsPeriodicPt (Pi.map f) n x :=
-  isPeriodicPt_piMap.mpr h
+theorem IsPeriodicPt.piMap (h : ∀ i, IsPeriodicPt (f i) n (x i)) :
+    IsPeriodicPt (Function.map f) n x := isPeriodicPt_piMap.mpr h
 
 end Pi
 
diff --git a/Mathlib/Dynamics/PeriodicPts/Lemmas.lean b/Mathlib/Dynamics/PeriodicPts/Lemmas.lean
index 8c3e8966981c3f..7d918179b284e4 100644
--- a/Mathlib/Dynamics/PeriodicPts/Lemmas.lean
+++ b/Mathlib/Dynamics/PeriodicPts/Lemmas.lean
@@ -141,16 +141,16 @@ variable {ι : Type*} {α : ι → Type*} {f : ∀ i, α i → α i} {x : ∀ i,
 /-- This `sInf` can be regarded as a generalized version of LCM
 for possibly infinite sets and types. -/
 theorem minimalPeriod_piMap :
-    minimalPeriod (Pi.map f) x = sInf { n > 0 | ∀ i, minimalPeriod (f i) (x i) ∣ n } := by
+    minimalPeriod (Function.map f) x = sInf { n > 0 | ∀ i, minimalPeriod (f i) (x i) ∣ n } := by
   conv_lhs => simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]
   simp [← isPeriodicPt_iff_minimalPeriod_dvd]
 
 theorem minimalPeriod_piMap_fintype [Fintype ι] :
-    minimalPeriod (Pi.map f) x = Finset.univ.lcm (fun i => minimalPeriod (f i) (x i)) :=
+    minimalPeriod (Function.map f) x = Finset.univ.lcm (fun i => minimalPeriod (f i) (x i)) :=
   eq_of_forall_dvd <| by simp [← isPeriodicPt_iff_minimalPeriod_dvd]
 
 theorem minimalPeriod_single_dvd_minimalPeriod_piMap (i : ι) :
-    minimalPeriod (f i) (x i) ∣ minimalPeriod (Pi.map f) x := by
+    minimalPeriod (f i) (x i) ∣ minimalPeriod (Function.map f) x := by
   simp only [minimalPeriod_piMap]
   by_cases h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
   · exact (Nat.sInf_mem h).2 i
diff --git a/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean b/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
index b82e2581436e08..0397e6a6b0fc0e 100644
--- a/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
+++ b/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
@@ -84,7 +84,7 @@ lemma IsDynCoverOf.preimage (h : Semiconj φ S T) [V.IsSymm] {t : Finset Y}
   choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ hy
   refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
   simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
-    mem_preimage, map_apply, exists_exists_and_eq_and]
+    mem_preimage, Prod.map_apply, exists_exists_and_eq_and]
   obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)
   refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩
   rw [φ_f _ (g_mem _ hy)]
diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean
index 3e55bcb56a8448..6f2509f8fef938 100644
--- a/Mathlib/FieldTheory/Perfect.lean
+++ b/Mathlib/FieldTheory/Perfect.lean
@@ -269,7 +269,7 @@ theorem injective_pow_p {x y : R} (h : x ^ p = y ^ p) : x = y := (frobeniusEquiv
 lemma polynomial_expand_eq (f : R[X]) :
     expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p := by
   rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
-    frobenius_comp_frobeniusEquiv_symm, map_id]
+    frobenius_comp_frobeniusEquiv_symm, Polynomial.map_id]
 
 @[simp]
 theorem not_irreducible_expand (R p) [CommSemiring R] [Fact p.Prime] [CharP R p] [PerfectRing R p]
@@ -421,7 +421,7 @@ theorem roots_X_pow_char_sub_C_pow {y : R} {m : ℕ} :
 theorem roots_expand_pow_map_iterateFrobenius :
     (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots := by
   simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
-    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
+    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, Multiset.map_id']
 
 theorem roots_expand_map_frobenius : (expand R p f).roots.map (frobenius R p) = p • f.roots := by
   simp [roots_expand, Multiset.map_nsmul]
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
index 06326309b3964c..895b9f93414220 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -417,10 +417,10 @@ theorem image_mem_nhdsWithin {x : H} {s : Set H} (hs : s ∈ 𝓝 x) : I '' s 
   I.map_nhds_eq x ▸ image_mem_map hs
 
 theorem symm_map_nhdsWithin_image {x : H} {s : Set H} : map I.symm (𝓝[I '' s] I x) = 𝓝[s] x := by
-  rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]
+  rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, Filter.map_id]
 
 theorem symm_map_nhdsWithin_range (x : H) : map I.symm (𝓝[range I] I x) = 𝓝 x := by
-  rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
+  rw [← I.map_nhds_eq, map_map, I.symm_comp_self, Filter.map_id]
 
 theorem uniqueDiffOn_preimage {s : Set H} (hs : IsOpen s) :
     UniqueDiffOn 𝕜 (I.symm ⁻¹' s ∩ range I) := by
diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index d8d869830ddd27..a2f5c0c6a18bc1 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -238,7 +238,7 @@ theorem map_extend_nhdsWithin {y : M} (hy : y ∈ f.source) :
 
 theorem map_extend_symm_nhdsWithin {y : M} (hy : y ∈ f.source) :
     map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y := by
-  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]
+  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, Filter.map_id]
   exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)
 
 theorem map_extend_symm_nhdsWithin_range {y : M} (hy : y ∈ f.source) :
diff --git a/Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean b/Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean
index 60a4982214b1f4..59d966b251e6e3 100644
--- a/Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean
@@ -34,7 +34,7 @@ open Finset in
 @[to_additive] protected theorem pi {ι : Type*} {M N : ι → Type*}
     [∀ i, CommMonoid (M i)] [∀ i, CommMonoid (N i)] (S : Π i, Submonoid (M i))
     {f : Π i, M i → N i} (hf : ∀ i, IsLocalizationMap (S i) (f i)) :
-    IsLocalizationMap (Submonoid.pi .univ S) (Pi.map f) where
+    IsLocalizationMap (Submonoid.pi .univ S) (Function.map f) where
   map_units m := Pi.isUnit_iff.mpr fun i ↦ (hf i).map_units ⟨_, m.2 i ⟨⟩⟩
   surj z := by
     choose x hx using fun i ↦ (hf i).surj
diff --git a/Mathlib/LinearAlgebra/Multilinear/Basis.lean b/Mathlib/LinearAlgebra/Multilinear/Basis.lean
index a9e58b86988345..3eb442db32e748 100644
--- a/Mathlib/LinearAlgebra/Multilinear/Basis.lean
+++ b/Mathlib/LinearAlgebra/Multilinear/Basis.lean
@@ -34,7 +34,7 @@ theorem Module.Basis.ext_multilinear [Finite ι] {f g : MultilinearMap R M N} {
   classical
   ext m
   rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
-  unfold Pi.map
+  unfold Function.map
   simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
     map_sum_finset, map_smul_univ, h]
 
diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean
index 3339eeaf6b43fd..c9cadb742c067e 100644
--- a/Mathlib/LinearAlgebra/Pi.lean
+++ b/Mathlib/LinearAlgebra/Pi.lean
@@ -126,7 +126,7 @@ instance CompatibleSMul.pi (R S M N ι : Type*) [Semiring S]
 
 /-- Construct a linear map between two (dependent) function spaces
 by applying index-dependent linear maps to the coordinates.
-A bundled version of `Pi.map`.
+A bundled version of `Function.map`.
 
 If the index type is finite, then this map can be seen as a “block diagonal” map
 between indexed products of modules. -/
@@ -136,7 +136,7 @@ def piMap {ψ : ι → Type*} [∀ i, AddCommMonoid (ψ i)] [∀ i, Module R (ψ
 
 @[simp]
 theorem coe_piMap {ψ : ι → Type*} [∀ i, AddCommMonoid (ψ i)] [∀ i, Module R (ψ i)]
-    (f : ∀ i, φ i →ₗ[R] ψ i) : ⇑(piMap f) = Pi.map fun i ↦ f i :=
+    (f : ∀ i, φ i →ₗ[R] ψ i) : ⇑(piMap f) = Function.map fun i ↦ f i :=
   rfl
 
 /-- Linear map between the function spaces `I → M₂` and `I → M₃`, induced by a linear map `f`
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index fbc5193ae2dbab..d6d2b6eaade657 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -141,7 +141,7 @@ section
 `∀ a, β₂ a`. -/
 @[simps (attr := grind =)]
 def piCongrRight {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (∀ a, β₁ a) ≃ (∀ a, β₂ a) :=
-  ⟨Pi.map fun a ↦ F a, Pi.map fun a ↦ (F a).symm, fun H => funext <| by simp,
+  ⟨Function.map fun a ↦ F a, Function.map fun a ↦ (F a).symm, fun H => funext <| by simp,
     fun H => funext <| by simp⟩
 
 @[simp]
@@ -908,7 +908,7 @@ theorem piCongr_symm_apply (f : ∀ b, Z b) :
 
 @[simp, grind =]
 theorem piCongr_apply_apply (f : ∀ a, W a) (a : α) : h₁.piCongr h₂ f (h₁ a) = h₂ a (f a) := by
-  rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
+  rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Function.map_apply]
 
 end
 
diff --git a/Mathlib/Logic/Equiv/PartialEquiv.lean b/Mathlib/Logic/Equiv/PartialEquiv.lean
index 579205b85614bd..04c0aba5a23966 100644
--- a/Mathlib/Logic/Equiv/PartialEquiv.lean
+++ b/Mathlib/Logic/Equiv/PartialEquiv.lean
@@ -847,8 +847,8 @@ variable {ι : Type*} {αi βi γi : ι → Type*}
 /-- The product of a family of partial equivalences, as a partial equivalence on the pi type. -/
 @[simps (attr := mfld_simps) -fullyApplied apply source target]
 protected def pi (ei : ∀ i, PartialEquiv (αi i) (βi i)) : PartialEquiv (∀ i, αi i) (∀ i, βi i) where
-  toFun := Pi.map fun i ↦ ei i
-  invFun := Pi.map fun i ↦ (ei i).symm
+  toFun := Function.map fun i ↦ ei i
+  invFun := Function.map fun i ↦ (ei i).symm
   source := pi univ fun i => (ei i).source
   target := pi univ fun i => (ei i).target
   map_source' _ hf i hi := (ei i).map_source (hf i hi)
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 6089b775ad276e..f63650a94c822b 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -218,7 +218,7 @@ theorem Injective.of_comp_iff' (f : α → β) {g : γ → α} (hg : Bijective g
   ⟨fun I ↦ I.of_comp_right hg.2, fun h ↦ h.comp hg.injective⟩
 
 theorem Injective.piMap {ι : Sort*} {α β : ι → Sort*} {f : ∀ i, α i → β i}
-    (hf : ∀ i, Injective (f i)) : Injective (Pi.map f) := fun _ _ h ↦
+    (hf : ∀ i, Injective (f i)) : Injective (Function.map f) := fun _ _ h ↦
   funext fun i ↦ hf i <| congrFun h _
 
 /-- Composition by an injective function on the left is itself injective. -/
@@ -592,7 +592,7 @@ theorem surjective_to_subsingleton [na : Nonempty α] [Subsingleton β] (f : α
   fun _ ↦ let ⟨a⟩ := na; ⟨a, Subsingleton.elim _ _⟩
 
 theorem Surjective.piMap {ι : Sort*} {α β : ι → Sort*} {f : ∀ i, α i → β i}
-    (hf : ∀ i, Surjective (f i)) : Surjective (Pi.map f) := fun g ↦
+    (hf : ∀ i, Surjective (f i)) : Surjective (Function.map f) := fun g ↦
   ⟨fun i ↦ surjInv (hf i) (g i), funext fun _ ↦ rightInverse_surjInv _ _⟩
 
 /-- Composition by a surjective function on the left is itself surjective. -/
@@ -607,7 +607,7 @@ theorem surjective_comp_left_iff [Nonempty α] {g : β → γ} :
   exact ⟨f a, congr_fun hf _⟩
 
 theorem Bijective.piMap {ι : Sort*} {α β : ι → Sort*} {f : ∀ i, α i → β i}
-    (hf : ∀ i, Bijective (f i)) : Bijective (Pi.map f) :=
+    (hf : ∀ i, Bijective (f i)) : Bijective (Function.map f) :=
   ⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2⟩
 
 /-- Composition by a bijective function on the left is itself bijective. -/
@@ -766,23 +766,23 @@ theorem update_idem {α} [DecidableEq α] {β : α → Sort*} {a : α} (v w : β
   grind
 
 @[simp]
-theorem _root_.Pi.map_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*}
+theorem map_const {ι : Sort*} {α} {β : ι → Sort*}
+    {f : ∀ i, α → β i} (a : α) :
+    Function.map f (Function.const ι a) = swap f a := rfl
+
+@[simp]
+theorem map_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*}
     {f : ∀ i, α i → β i}
     (g : ∀ i, α i) (i : ι) (a : α i) :
-    Pi.map f (Function.update g i a) = Function.update (Pi.map f g) i (f i a) := by
-  ext j
-  obtain rfl | hij := eq_or_ne j i <;> simp [*]
+    Function.map f (Function.update g i a) = Function.update (Function.map f g) i (f i a) := by
+  grind [Function.update]
 
 @[simp]
-theorem _root_.Pi.map_injective
+theorem map_injective
     {ι : Sort*} {α β : ι → Sort*} [∀ i, Nonempty (α i)] {f : ∀ i, α i → β i} :
-    Injective (Pi.map f) ↔ ∀ i, Injective (f i) where
-  mp h i x y hxy := by
-    classical
-    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
-    replace h := @h (Function.update default i x) (Function.update default i y) ?_
-    · simpa using congrFun h i
-    rw [Pi.map_update, Pi.map_update, hxy]
+    Injective (Function.map f) ↔ ∀ i, Injective (f i) where
+  mp h i x y hxy := by classical exact Function.update_injective Classical.ofNonempty i <| h <|
+    (map_update _ _ x ▸ map_update _ _ y ▸ hxy ▸ rfl)
   mpr := .piMap
 
 end Update
@@ -1090,6 +1090,14 @@ theorem sometimes_spec {p : Prop} {α} [Nonempty α] (P : α → Prop) (f : p 
 
 end Sometimes
 
+@[simp] theorem map_id {ι} {α : ι → Type*} : Function.map (fun i => @id (α i)) = id := rfl
+
+@[simp] theorem map_id' {ι} {α : ι → Type*} : Function.map (fun i (a : α i) => a) = fun x ↦ x := rfl
+
+theorem map_comp_map {ι} {α β γ : ι → Type*} (f : ∀ i, α i → β i) (g : ∀ i, β i → γ i) :
+    Function.map g ∘ Function.map f = Function.map fun i => g i ∘ f i :=
+  rfl
+
 end Function
 
 variable {α β : Sort*}
@@ -1200,16 +1208,17 @@ instance {α β : Type*} {r : α × β → Prop} {a : α} {b : β} [Decidable (r
     Decidable (curry r a b) :=
   ‹Decidable _›
 
-namespace Pi
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_id := Function.map_id
 
-variable {ι : Type*}
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_id' := Function.map_id'
 
-@[simp] theorem map_id {α : ι → Type*} : Pi.map (fun i => @id (α i)) = id := rfl
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_comp_map := Function.map_comp_map
 
-@[simp] theorem map_id' {α : ι → Type*} : Pi.map (fun i (a : α i) => a) = fun x ↦ x := rfl
-
-theorem map_comp_map {α β γ : ι → Type*} (f : ∀ i, α i → β i) (g : ∀ i, β i → γ i) :
-    Pi.map g ∘ Pi.map f = Pi.map fun i => g i ∘ f i :=
-  rfl
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_injective := Function.map_injective
 
-end Pi
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_update := Function.map_update
diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean
index 04b9b63554da8d..42fb0f28af2072 100644
--- a/Mathlib/Logic/Function/Defs.lean
+++ b/Mathlib/Logic/Function/Defs.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 module
 
 public import Mathlib.Init
-
+public import Batteries.Tactic.Alias
 import Mathlib.Tactic.Attr.Register
 
 /-!
@@ -134,17 +134,22 @@ theorem isFixedPt_id (x : α) : IsFixedPt id x :=
 @[simp] theorem forall_isFixedPt_iff {f : α → α} : (∀ x, IsFixedPt f x) ↔ f = id :=
   ⟨funext, fun h ↦ h ▸ isFixedPt_id⟩
 
-end Function
+/-- Sends a dependent function `a : ∀ i, α i` to a dependent function `Function.map f a : ∀ i, β i`
+by applying `f i` to `i`-th component. -/
+protected def map {ι} {α β : ι → Sort*} (f : ∀ i, α i → β i) : (∀ i, α i) → (∀ i, β i) :=
+  fun a i ↦ f i (a i)
 
-namespace Pi
+lemma map_def {ι} {α β : ι → Sort*} (f : ∀ i, α i → β i) (g : ∀ i, α i) :
+    Function.map f g = (fun {i} => f i) ∘' g := rfl
 
-variable {ι : Sort*} {α β : ι → Sort*}
+@[simp, grind =]
+lemma map_apply {ι} {α β : ι → Sort*} (f : ∀ i, α i → β i) (a : ∀ i, α i) (i : ι) :
+    Function.map f a i = f i (a i) := rfl
 
-/-- Sends a dependent function `a : ∀ i, α i` to a dependent function `Pi.map f a : ∀ i, β i`
-by applying `f i` to `i`-th component. -/
-protected def map (f : ∀ i, α i → β i) : (∀ i, α i) → (∀ i, β i) := fun a i ↦ f i (a i)
+end Function
 
-@[simp]
-lemma map_apply (f : ∀ i, α i → β i) (a : ∀ i, α i) (i : ι) : Pi.map f a i = f i (a i) := rfl
+@[deprecated (since := "2026-05-11")]
+alias Pi.map := Function.map
 
-end Pi
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_apply := Function.map_apply
diff --git a/Mathlib/Logic/Function/Iterate.lean b/Mathlib/Logic/Function/Iterate.lean
index 48324196626b2d..b159037c401ad8 100644
--- a/Mathlib/Logic/Function/Iterate.lean
+++ b/Mathlib/Logic/Function/Iterate.lean
@@ -224,6 +224,11 @@ lemma iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a =
 theorem involutive_iff_iter_2_eq_id {α} {f : α → α} : Involutive f ↔ f^[2] = id :=
   funext_iff.symm
 
+@[simp]
+theorem map_iterate {ι : Type*} {α : ι → Type*} (f : ∀ i, α i → α i) (n : ℕ) :
+    (Function.map f)^[n] = Function.map fun i => (f i)^[n] := by
+  induction n <;> simp [*, map_comp_map]
+
 end Function
 
 namespace List
@@ -242,13 +247,5 @@ theorem foldr_const (f : β → β) (b : β) : ∀ l : List α, l.foldr (fun _ 
 
 end List
 
-namespace Pi
-
-variable {ι : Type*}
-
-@[simp]
-theorem map_iterate {α : ι → Type*} (f : ∀ i, α i → α i) (n : ℕ) :
-    (Pi.map f)^[n] = Pi.map fun i => (f i)^[n] := by
-  induction n <;> simp [*, map_comp_map]
-
-end Pi
+@[deprecated (since := "2026-05-11")]
+alias Pi.map_iterate := Function.map_iterate
diff --git a/Mathlib/Order/Filter/Cofinite.lean b/Mathlib/Order/Filter/Cofinite.lean
index d5a8fc34d8e2c9..0ef62544d15664 100644
--- a/Mathlib/Order/Filter/Cofinite.lean
+++ b/Mathlib/Order/Filter/Cofinite.lean
@@ -165,7 +165,7 @@ See also `map_piMap_pi_finite` for the case of a finite index type.
 -/
 theorem map_piMap_pi {α β : ι → Type*} {f : ∀ i, α i → β i}
     (hf : ∀ᶠ i in cofinite, Surjective (f i)) (l : ∀ i, Filter (α i)) :
-    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) := by
+    map (Function.map f) (pi l) = pi fun i ↦ map (f i) (l i) := by
   refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_
   refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_
   rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩
@@ -186,7 +186,7 @@ See also `map_piMap_pi` for a more general case.
 -/
 theorem map_piMap_pi_finite {α β : ι → Type*} [Finite ι]
     (f : ∀ i, α i → β i) (l : ∀ i, Filter (α i)) :
-    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
+    map (Function.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
   map_piMap_pi (by simp) l
 
 end Filter
diff --git a/Mathlib/Order/Filter/Pi.lean b/Mathlib/Order/Filter/Pi.lean
index 7374aa9ad521b2..d4199718af5ad1 100644
--- a/Mathlib/Order/Filter/Pi.lean
+++ b/Mathlib/Order/Filter/Pi.lean
@@ -250,11 +250,11 @@ theorem pi_inj [∀ i, NeBot (f₁ i)] : pi f₁ = pi f₂ ↔ f₁ = f₂ := by
 
 theorem tendsto_piMap_pi {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (α i)}
     {l' : ∀ i, Filter (β i)} (h : ∀ i, Tendsto (f i) (l i) (l' i)) :
-    Tendsto (Pi.map f) (pi l) (pi l') :=
+    Tendsto (Function.map f) (pi l) (pi l') :=
   tendsto_pi.2 fun i ↦ (h i).comp (tendsto_eval_pi _ _)
 
 theorem pi_comap {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (β i)} :
-    pi (fun i ↦ comap (f i) (l i)) = comap (Pi.map f) (pi l) := by
+    pi (fun i ↦ comap (f i) (l i)) = comap (Function.map f) (pi l) := by
   simp [Filter.pi, Filter.comap_comap, Function.comp_def]
 
 end Pi
diff --git a/Mathlib/RingTheory/Coalgebra/Basic.lean b/Mathlib/RingTheory/Coalgebra/Basic.lean
index 3b112f5f9ec757..cb09522524d683 100644
--- a/Mathlib/RingTheory/Coalgebra/Basic.lean
+++ b/Mathlib/RingTheory/Coalgebra/Basic.lean
@@ -443,22 +443,22 @@ section coalgebraStruct
 variable [Π i, CoalgebraStruct R (A i)]
 
 instance instCoalgebraStruct : CoalgebraStruct R (Π i, A i) where
-  comul := .lsum R _ R fun i ↦ map (.single R _ i) (.single R _ i) ∘ₗ comul
+  comul := .lsum R _ R fun i ↦ TensorProduct.map (.single R _ i) (.single R _ i) ∘ₗ comul
   counit := .lsum R _ R fun _ ↦ counit
 
 @[simp] theorem comul_single (i : n) (a : A i) :
-    comul (single i a) = map (.single R _ i) (.single R _ i) (comul a) :=
+    comul (single i a) = TensorProduct.map (.single R _ i) (.single R _ i) (comul a) :=
   lsum_piSingle _ _ _ _ _ _
 
 @[simp] theorem counit_single (i : n) (a : A i) : counit (single i a) = counit (R := R) a :=
   lsum_piSingle _ _ _ _ _ _
 
 theorem comul_comp_single (i : n) :
-    comul ∘ₗ .single R _ i = map (.single R A i) (.single R A i) ∘ₗ comul := by
+    comul ∘ₗ .single R _ i = TensorProduct.map (.single R A i) (.single R A i) ∘ₗ comul := by
   ext; simp
 
 theorem comul_comp_proj (i : n) :
-    comul ∘ₗ (proj i : (Π i, A i) →ₗ[R] A i) = map (proj i) (proj i) ∘ₗ comul := by
+    comul ∘ₗ (proj i : (Π i, A i) →ₗ[R] A i) = TensorProduct.map (proj i) (proj i) ∘ₗ comul := by
   ext j; have := eq_or_ne i j
   aesop (add simp [map_map, proj_comp_single, diag])
 
@@ -477,7 +477,7 @@ theorem counit_comp_dFinsuppCoeFnLinearMap :
 open DFinsupp in
 theorem comul_comp_dFinsuppCoeFnLinearMap :
     comul (R := R) (A := Π i, A i) ∘ₗ coeFnLinearMap _ =
-      map (coeFnLinearMap _) (coeFnLinearMap _) ∘ₗ comul := by
+      TensorProduct.map (coeFnLinearMap _) (coeFnLinearMap _) ∘ₗ comul := by
   apply LinearMap.ext fun x ↦ ?_
   have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _
   rw [← DFinsupp.sum_single (f := x)]
@@ -485,7 +485,7 @@ theorem comul_comp_dFinsuppCoeFnLinearMap :
 
 open DFinsupp in
 @[simp] theorem comul_coe_dFinsupp (x : Π₀ i, A i) :
-    comul (R := R) ⇑x = map (coeFnLinearMap _) (coeFnLinearMap _) (comul x) :=
+    comul (R := R) ⇑x = TensorProduct.map (coeFnLinearMap _) (coeFnLinearMap _) (comul x) :=
   congr($comul_comp_dFinsuppCoeFnLinearMap x)
 
 variable {M : Type*} [AddCommMonoid M] [Module R M] [CoalgebraStruct R M]
@@ -501,14 +501,14 @@ theorem counit_comp_finsuppLcoeFun :
 
 open Finsupp in
 theorem comul_comp_finsuppLcoeFun :
-    comul (R := R) (A := n → M) ∘ₗ lcoeFun = map lcoeFun lcoeFun ∘ₗ comul := by
+    comul (R := R) (A := n → M) ∘ₗ lcoeFun = TensorProduct.map lcoeFun lcoeFun ∘ₗ comul := by
   apply LinearMap.ext fun x ↦ ?_
   rw [← Finsupp.univ_sum_single x]
   simp [-univ_sum_single, single_eq_pi_single, map_map]
 
 open Finsupp in
 @[simp] theorem comul_coe_finsupp (x : n →₀ M) :
-    comul (R := R) ⇑x = map lcoeFun lcoeFun (comul x) :=
+    comul (R := R) ⇑x = TensorProduct.map lcoeFun lcoeFun (comul x) :=
   congr($comul_comp_finsuppLcoeFun x)
 
 end coalgebraStruct
diff --git a/Mathlib/Topology/Algebra/FilterBasis.lean b/Mathlib/Topology/Algebra/FilterBasis.lean
index 4fb7ef63e1ba8c..9932c213f4fa1b 100644
--- a/Mathlib/Topology/Algebra/FilterBasis.lean
+++ b/Mathlib/Topology/Algebra/FilterBasis.lean
@@ -130,7 +130,7 @@ def N (B : GroupFilterBasis G) : G → Filter G :=
 
 @[to_additive (attr := simp)]
 theorem N_one (B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter := by
-  simp only [N, one_mul, map_id']
+  simp only [N, one_mul, Filter.map_id']
 
 @[to_additive]
 protected theorem hasBasis (B : GroupFilterBasis G) (x : G) :
diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
index 81c1fb72e14aef..184c002d7d098b 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
@@ -218,7 +218,7 @@ variable {ψ : ι → Type*} [∀ i, TopologicalSpace (ψ i)] [∀ i, AddCommMon
 
 /-- Construct a continuous linear map between two (dependent) function spaces
 by applying index-dependent linear maps to the coordinates.
-A bundled version of `Pi.map`.
+A bundled version of `Function.map`.
 
 If the index type is finite, then this map can be seen as a “block diagonal” map
 between indexed products of modules. -/
@@ -231,7 +231,7 @@ theorem coe_piMap (f : ∀ i, φ i →L[R] ψ i) :
   rfl
 
 @[simp]
-theorem coe_piMap' (f : ∀ i, φ i →L[R] ψ i) : ⇑(piMap f) = Pi.map fun i ↦ f i :=
+theorem coe_piMap' (f : ∀ i, φ i →L[R] ψ i) : ⇑(piMap f) = Function.map fun i ↦ f i :=
   rfl
 
 end PiMap
diff --git a/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean b/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
index bda5e04f0ef950..3ee5515058a3f5 100644
--- a/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
+++ b/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
@@ -489,8 +489,8 @@ theorem continuous_dom_pi {n : Type*} [Finite n] {X : Type*}
     {C : (j : n) → (i : ι) → Set (A j i)}
     (hCopen : ∀ j i, IsOpen (C j i))
     {f : (Π j : n, Πʳ i : ι, [A j i, C j i]) → X} :
-    Continuous f ↔
-      ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous (f ∘ Pi.map fun _ ↦ inclusion _ _ hS) := by
+    Continuous f ↔ ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
+      Continuous (f ∘ Function.map fun _ ↦ inclusion _ _ hS) := by
   refine ⟨by fun_prop, fun H ↦ ?_⟩
   simp_rw [continuous_iff_continuousAt, ContinuousAt]
   intro x
@@ -500,9 +500,9 @@ theorem continuous_dom_pi {n : Type*} [Finite n] {X : Type*}
     change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i
     simp [-eventually_cofinite]
   let x' (j : n) : Πʳ i : ι, [A j i, C j i]_[𝓟 S] := .mk (fun i ↦ x j i) (fun i hi ↦ hi _)
-  have hxx' : Pi.map (fun j ↦ inclusion _ _ hS) x' = x := rfl
-  simp_rw [← hxx', nhds_pi, Pi.map_apply, nhds_eq_map_inclusion (hCopen _), ← map_piMap_pi_finite,
-    tendsto_map'_iff, ← nhds_pi]
+  have hxx' : Function.map (fun j ↦ inclusion _ _ hS) x' = x := rfl
+  simp_rw [← hxx', nhds_pi, Function.map_apply, nhds_eq_map_inclusion (hCopen _),
+    ← map_piMap_pi_finite, tendsto_map'_iff, ← nhds_pi]
   exact (H _ _).tendsto _
 
 end cofinite
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index 6f88474bbad152..75f1ac11f446f2 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -755,7 +755,7 @@ theorem Filter.Tendsto.apply_nhds {l : Filter Y} {f : Y → ∀ i, A i} {x : ∀
 
 @[fun_prop]
 protected theorem Continuous.piMap
-    {f : ∀ i, A i → B i} (hf : ∀ i, Continuous (f i)) : Continuous (Pi.map f) :=
+    {f : ∀ i, A i → B i} (hf : ∀ i, Continuous (f i)) : Continuous (Function.map f) :=
   continuous_pi fun i ↦ (hf i).comp (continuous_apply i)
 
 theorem nhds_pi {a : ∀ i, A i} : 𝓝 a = pi fun i => 𝓝 (a i) := by
@@ -763,13 +763,13 @@ theorem nhds_pi {a : ∀ i, A i} : 𝓝 a = pi fun i => 𝓝 (a i) := by
 
 protected theorem IsOpenMap.piMap {f : ∀ i, A i → B i}
     (hfo : ∀ i, IsOpenMap (f i)) (hsurj : ∀ᶠ i in cofinite, Surjective (f i)) :
-    IsOpenMap (Pi.map f) := by
+    IsOpenMap (Function.map f) := by
   refine IsOpenMap.of_nhds_le fun x ↦ ?_
   rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]
   exact Filter.pi_mono fun i ↦ (hfo i).nhds_le _
 
 protected theorem IsOpenQuotientMap.piMap
-    {f : ∀ i, A i → B i} (hf : ∀ i, IsOpenQuotientMap (f i)) : IsOpenQuotientMap (Pi.map f) :=
+    {f : ∀ i, A i → B i} (hf : ∀ i, IsOpenQuotientMap (f i)) : IsOpenQuotientMap (Function.map f) :=
   ⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2, .piMap (fun i ↦ (hf i).3) <|
     .of_forall fun i ↦ (hf i).1⟩
 
@@ -789,15 +789,15 @@ theorem continuousAt_pi' {f : X → ∀ i, A i} {x : X} (hf : ∀ i, ContinuousA
 @[fun_prop]
 protected theorem ContinuousAt.piMap {f : ∀ i, A i → B i} {x : ∀ i, A i}
     (hf : ∀ i, ContinuousAt (f i) (x i)) :
-    ContinuousAt (Pi.map f) x :=
+    ContinuousAt (Function.map f) x :=
   continuousAt_pi.2 fun i ↦ (hf i).comp (continuousAt_apply i x)
 
 protected lemma Topology.IsInducing.piMap {f : ∀ i, A i → B i}
-    (hf : ∀ i, IsInducing (f i)) : IsInducing (Pi.map f) := by
+    (hf : ∀ i, IsInducing (f i)) : IsInducing (Function.map f) := by
   simp [isInducing_iff_nhds, nhds_pi, (hf _).nhds_eq_comap, Filter.pi_comap]
 
 protected lemma Topology.IsEmbedding.piMap {f : ∀ i, A i → B i}
-    (hf : ∀ i, IsEmbedding (f i)) : IsEmbedding (Pi.map f) :=
+    (hf : ∀ i, IsEmbedding (f i)) : IsEmbedding (Function.map f) :=
   ⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2⟩
 
 theorem Pi.continuous_precomp' {ι' : Type*} (φ : ι' → ι) :
@@ -1072,11 +1072,11 @@ theorem isClosed_set_pi {i : Set ι} {s : ∀ a, Set (A a)} (hs : ∀ a ∈ i, I
   rw [pi_def]; exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)
 
 protected lemma Topology.IsClosedEmbedding.piMap {f : ∀ i, A i → B i}
-    (hf : ∀ i, IsClosedEmbedding (f i)) : IsClosedEmbedding (Pi.map f) :=
+    (hf : ∀ i, IsClosedEmbedding (f i)) : IsClosedEmbedding (Function.map f) :=
   ⟨.piMap fun i ↦ (hf i).1, by simpa using isClosed_set_pi fun i _ ↦ (hf i).2⟩
 
 protected lemma Topology.IsOpenEmbedding.piMap [Finite ι] {f : ∀ i, A i → B i}
-    (hf : ∀ i, IsOpenEmbedding (f i)) : IsOpenEmbedding (Pi.map f) :=
+    (hf : ∀ i, IsOpenEmbedding (f i)) : IsOpenEmbedding (Function.map f) :=
   ⟨.piMap fun i ↦ (hf i).1, by simpa using isOpen_set_pi Set.finite_univ fun i _ ↦ (hf i).2⟩
 
 theorem mem_nhds_of_pi_mem_nhds {I : Set ι} {s : ∀ i, Set (A i)} (a : ∀ i, A i) (hs : I.pi s ∈ 𝓝 a)
diff --git a/Mathlib/Topology/Maps/Basic.lean b/Mathlib/Topology/Maps/Basic.lean
index 9a4a5b10c48085..a6a088acade335 100644
--- a/Mathlib/Topology/Maps/Basic.lean
+++ b/Mathlib/Topology/Maps/Basic.lean
@@ -395,7 +395,7 @@ theorem of_sections
   of_nhds_le fun x =>
     let ⟨g, hgc, hgx, hgf⟩ := h x
     calc
-      𝓝 (f x) = map f (map g (𝓝 (f x))) := by rw [map_map, hgf.comp_eq_id, map_id]
+      𝓝 (f x) = map f (map g (𝓝 (f x))) := by rw [map_map, hgf.comp_eq_id, Filter.map_id]
       _ ≤ map f (𝓝 (g (f x))) := map_mono hgc
       _ = map f (𝓝 x) := by rw [hgx]
 
diff --git a/Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean b/Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean
index 31e0cbf3018746..2f79752a04c9b5 100644
--- a/Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean
+++ b/Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean
@@ -58,7 +58,7 @@ open Real
 
 /-- A continuous surjection from the Cantor space to the Hilbert cube. -/
 noncomputable def cantorToHilbert (x : ℕ → Bool) : ℕ → unitInterval :=
-  Pi.map (fun _ b ↦ fromBinary b) (cantorSpaceHomeomorphNatToCantorSpace x)
+  Function.map (fun _ b ↦ fromBinary b) (cantorSpaceHomeomorphNatToCantorSpace x)
 
 theorem cantorToHilbert_continuous : Continuous cantorToHilbert :=
   continuous_pi (fun _ ↦ fromBinary_continuous.comp (by fun_prop))
diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean
index 0fdbb686f4ca3f..34f21ecff1766c 100644
--- a/Mathlib/Topology/MetricSpace/Isometry.lean
+++ b/Mathlib/Topology/MetricSpace/Isometry.lean
@@ -94,8 +94,8 @@ theorem prodMap {δ} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf
 
 protected theorem piMap {ι} [Fintype ι] {α β : ι → Type*} [∀ i, PseudoEMetricSpace (α i)]
     [∀ i, PseudoEMetricSpace (β i)] (f : ∀ i, α i → β i) (hf : ∀ i, Isometry (f i)) :
-    Isometry (Pi.map f) := fun x y => by
-  simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]
+    Isometry (Function.map f) := fun x y => by
+  simp only [edist_pi_def, (hf _).edist_eq, Function.map_apply]
 
 protected lemma single [Fintype ι] [DecidableEq ι] {E : ι → Type*} [∀ i, PseudoEMetricSpace (E i)]
     [∀ i, Zero (E i)] (i : ι) :
diff --git a/Mathlib/Topology/NhdsWithin.lean b/Mathlib/Topology/NhdsWithin.lean
index 1d466b1745e331..b2f7c1512611b3 100644
--- a/Mathlib/Topology/NhdsWithin.lean
+++ b/Mathlib/Topology/NhdsWithin.lean
@@ -419,7 +419,7 @@ theorem dense_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i
 
 theorem DenseRange.piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)]
     {f : (i : ι) → (X i) → (Y i)} (hf : ∀ i, DenseRange (f i)) :
-    DenseRange (Pi.map f) := by
+    DenseRange (Function.map f) := by
   rw [DenseRange, Set.range_piMap]
   exact dense_pi Set.univ (fun i _ => hf i)