feat: Pi.map rename to Function.map

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

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

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⟩

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

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]

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

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 =

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
 

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⟩ :=

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₂) :=

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

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) :=

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
 

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

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)]

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]

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

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) :

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

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]
 

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`

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
 

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)