diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean
index 85393a4cd9d432..0cb732b074509d 100644
--- a/Mathlib/Analysis/InnerProductSpace/Calculus.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Calculus.lean
@@ -389,7 +389,7 @@ theorem contDiffOn_univBall_symm :
   unfold univBall; split_ifs with h
   · refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
     rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
-    apply OpenPartialHomeomorph.symm_mapsTo
+    apply OpenPartialHomeomorph.mapsTo_symm
   · exact contDiffOn_id.sub contDiffOn_const
 
 end OpenPartialHomeomorph
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
index 224c9ebd3782a3..ea2e188c661437 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -271,8 +271,9 @@ theorem contMDiffWithinAt_iff_target :
         ContinuousWithinAt f s x :=
       and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
   simp_rw [cont, ContDiffWithinAtProp, extChartAt, OpenPartialHomeomorph.extend,
-    PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe,
-    modelWithCornersSelf_coe, chartAt_self_eq, OpenPartialHomeomorph.refl_apply, id_comp]
+    PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe,
+    OpenPartialHomeomorph.coe_toPartialEquiv, modelWithCornersSelf_coe, chartAt_self_eq,
+    OpenPartialHomeomorph.refl_apply, id_comp]
   rfl
 
 theorem contMDiffAt_iff_target {x : M} :
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
index 126498eec36f50..e6ab158996ea6c 100644
--- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
@@ -456,7 +456,7 @@ lemma contMDiff_equivTangentBundleProd_symm :
       with p hp
     -- now we have to check that the original map coincides locally with `pM` read in target chart.
     simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
-      PartialEquiv.prod_source, Set.mem_prod, TangentBundle.mem_chart_source_iff] at hp
+      PartialEquiv.prod_source, mem_prod, TangentBundle.mem_chart_source_iff] at hp
     let φ (x : E) := I ((chartAt H a.proj) ((chartAt H p.1.proj).symm (I.symm x)))
     have D0 : DifferentiableWithinAt 𝕜 φ (Set.range I) (I ((chartAt H p.1.proj) p.1.proj)) := by
       apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
@@ -495,7 +495,7 @@ lemma contMDiff_equivTangentBundleProd_symm :
       with p hp
     -- now we have to check that the original map coincides locally with `pM'` read in target chart.
     simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
-      PartialEquiv.prod_source, Set.mem_prod, TangentBundle.mem_chart_source_iff] at hp
+      PartialEquiv.prod_source, mem_prod, TangentBundle.mem_chart_source_iff] at hp
     let φ (x : E') := I' ((chartAt H' b.proj) ((chartAt H' p.2.proj).symm (I'.symm x)))
     have D0 : DifferentiableWithinAt 𝕜 φ (Set.range I') (I' ((chartAt H' p.2.proj) p.2.proj)) := by
       apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean
index ac1cf5c733ae4a..6711077b3caad1 100644
--- a/Mathlib/Geometry/Manifold/Instances/Icc.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Icc.lean
@@ -76,10 +76,10 @@ lemma contMDiff_subtype_coe_Icc : CMDiff n (fun (z : Icc x y) ↦ (z : ℝ)) :=
   suffices ContDiffWithinAt ℝ n _ (range ↑(𝓡∂ 1)) _ by simpa
   split_ifs with hz
   · simp? [IccLeftChart, Function.comp_def, modelWithCornersEuclideanHalfSpace] says
-      simp only [IccLeftChart, Fin.isValue, OpenPartialHomeomorph.mk_coe_symm,
+      simp only [IccLeftChart, Fin.isValue, OpenPartialHomeomorph.coe_mk_symm,
         PartialEquiv.coe_symm_mk, modelWithCornersEuclideanHalfSpace, ModelWithCorners.mk_symm,
         Function.comp_def, Function.update_self, ModelWithCorners.mk_coe,
-        OpenPartialHomeomorph.mk_coe]
+        OpenPartialHomeomorph.coe_mk]
     rw [Subtype.range_val_subtype]
     have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z 0 + x) := by fun_prop
     apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem; swap
@@ -92,10 +92,10 @@ lemma contMDiff_subtype_coe_Icc : CMDiff n (fun (z : Icc x y) ↦ (z : ℝ)) :=
     linarith
   · simp only [not_lt] at hz
     simp? [IccRightChart, Function.comp_def, modelWithCornersEuclideanHalfSpace] says
-      simp only [IccRightChart, Fin.isValue, OpenPartialHomeomorph.mk_coe_symm,
+      simp only [IccRightChart, Fin.isValue, OpenPartialHomeomorph.coe_mk_symm,
         PartialEquiv.coe_symm_mk, modelWithCornersEuclideanHalfSpace, ModelWithCorners.mk_symm,
         Function.comp_def, Function.update_self, ModelWithCorners.mk_coe,
-        OpenPartialHomeomorph.mk_coe]
+        OpenPartialHomeomorph.coe_mk]
     rw [Subtype.range_val_subtype]
     have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z 0) := by fun_prop
     apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem; swap
diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
index e4a64c4977d88e..931be7ae7c4abb 100644
--- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -411,7 +411,7 @@ instance EuclideanSpace.instIsManifoldSphere
         PartialEquiv.symm_source, stereographic'_target, stereographic'_source]
       simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm,
         Set.range_id, Set.inter_univ, Set.univ_inter, Set.compl_singleton_eq, Set.preimage_setOf_eq]
-      simp only [id, comp_apply, OpenPartialHomeomorph.coe_coe_symm,
+      simp only [id, comp_apply, OpenPartialHomeomorph.coe_toPartialEquiv_symm,
         innerSL_apply_apply, Ne, sphere_ext_iff, real_inner_comm (v' : E)]
       rfl)
 
diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
index b2581f57d9c419..0388d393f42a59 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
@@ -408,7 +408,7 @@ lemma isInvertible_fderivWithin_extendCoordChange (hn : n ≠ 0)
     · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
     · exact (φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn) :)
     · exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn
-    · exact φ.symm_mapsTo
+    · exact φ.mapsTo_symm
     · exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)
   · rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
     · exact I.uniqueDiffOn_extendCoordChange_source _ hx
diff --git a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
index 95b2e6e2256aad..fbbf24bbcdbee8 100644
--- a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
+++ b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
@@ -340,7 +340,7 @@ def IsLocalDiffeomorph.diffeomorphOfBijective
   have aux (x) : EqOn g (Φ x).symm (Φ x).target :=
     eqOn_of_leftInvOn_of_rightInvOn (fun x' _ ↦ hgInverse.1 x')
       (LeftInvOn.congr_left ((Φ x).toOpenPartialHomeomorph).rightInvOn
-        ((Φ x).toOpenPartialHomeomorph).symm_mapsTo (hyp x).2.symm)
+        ((Φ x).toOpenPartialHomeomorph).mapsTo_symm (hyp x).2.symm)
       (fun _y hy ↦ (Φ x).map_target hy)
   exact {
     toFun := f
diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
index 7549d6ab48b275..515811046a401e 100644
--- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
+++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
@@ -337,7 +337,7 @@ theorem liftPropOn_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈
     (hf : f ∈ G'.maximalAtlas M') (h : LiftPropOn P g s) {y : H}
     (hy : y ∈ e.target ∩ e.symm ⁻¹' (s ∩ g ⁻¹' f.source)) :
     P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) y := by
-  convert! ((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).2
+  convert! ((hG.liftPropWithinAt_indep_chart he (e.mapsTo_symm hy.1) hf hy.2.2).1 (h _ hy.2.1)).2
   rw [e.right_inv hy.1]
 
 theorem liftPropWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
index 40e6c12f40a815..88a224e75a99d4 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
@@ -223,9 +223,9 @@ theorem mdifferentiableWithinAt_iff_target :
         ContinuousWithinAt f s x :=
       and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
   simp_rw [cont, DifferentiableWithinAtProp, extChartAt, OpenPartialHomeomorph.extend,
-    PartialEquiv.coe_trans,
-    ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
-    chartAt_self_eq, OpenPartialHomeomorph.refl_apply]
+    PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe,
+    OpenPartialHomeomorph.coe_toPartialEquiv, modelWithCornersSelf_coe, chartAt_self_eq,
+    OpenPartialHomeomorph.refl_apply]
   rfl
 
 theorem mdifferentiableAt_iff_target {x : M} :
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
index 620ac719fb7b7a..e120727df246fe 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
@@ -188,7 +188,7 @@ theorem contMDiffWithinAt_totalSpace {f : M → TotalSpace F E} {s : Set M} {x
     ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
       ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
   refine EventuallyEq.contMDiffWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
-  · simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]
+  · simp_rw [Function.comp, OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe]
     rw [Trivialization.coe_fst']
     exact hx
   · simp only [mfld_simps]
@@ -498,7 +498,7 @@ theorem contMDiffOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
 
 theorem contMDiffOn_symm (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
     ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n e.toOpenPartialHomeomorph.symm e.target := by
-  rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.symm_mapsTo]
+  rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.mapsTo_symm]
   refine ⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
     contMDiffOn_snd.congr fun x hx ↦ ?_⟩
   rw [e.apply_symm_apply hx]
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
index a5e4beb9802d20..3bf5e2e868d6de 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
@@ -54,7 +54,7 @@ theorem mdifferentiableWithinAt_totalSpace (f : M → TotalSpace F E) {s : Set M
     ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
       ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
   refine EventuallyEq.mdifferentiableWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
-  · simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]
+  · simp_rw [Function.comp, OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe]
     rw [Trivialization.coe_fst']
     exact hx
   · simp only [mfld_simps]
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
index b52f954aa8e8b2..1edc7deffc77e7 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
@@ -377,13 +377,13 @@ theorem tangentBundle_model_space_chartAt (p : TangentBundle I H) :
 @[simp, mfld_simps]
 theorem tangentBundle_model_space_coe_chartAt (p : TangentBundle I H) :
     ⇑(chartAt (ModelProd H E) p) = TotalSpace.toProd H E := by
-  rw [← OpenPartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt]; rfl
+  rw [← OpenPartialHomeomorph.coe_toPartialEquiv, tangentBundle_model_space_chartAt]; rfl
 
 @[simp, mfld_simps]
 theorem tangentBundle_model_space_coe_chartAt_symm (p : TangentBundle I H) :
     ((chartAt (ModelProd H E) p).symm : ModelProd H E → TangentBundle I H) =
       (TotalSpace.toProd H E).symm := by
-  rw [← OpenPartialHomeomorph.coe_coe, OpenPartialHomeomorph.symm_toPartialEquiv,
+  rw [← OpenPartialHomeomorph.coe_toPartialEquiv, OpenPartialHomeomorph.symm_toPartialEquiv,
     tangentBundle_model_space_chartAt]; rfl
 
 theorem tangentBundleCore_coordChange_model_space (x x' z : H) :
diff --git a/Mathlib/Logic/Equiv/PartialEquiv.lean b/Mathlib/Logic/Equiv/PartialEquiv.lean
index 579205b85614bd..ab5a1e63ed1657 100644
--- a/Mathlib/Logic/Equiv/PartialEquiv.lean
+++ b/Mathlib/Logic/Equiv/PartialEquiv.lean
@@ -204,9 +204,11 @@ theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.targ
 
 protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 
-theorem symm_mapsTo : MapsTo e.symm e.target e.source :=
+theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
   e.symm.mapsTo
 
+@[deprecated (since := "2026-05-18")] alias symm_mapsTo := mapsTo_symm
+
 protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv
 
 protected theorem rightInvOn : RightInvOn e.symm e e.target := fun _ => e.right_inv
@@ -218,7 +220,7 @@ protected theorem injOn : InjOn e e.source :=
   e.leftInvOn.injOn
 
 protected theorem bijOn : BijOn e e.source e.target :=
-  e.invOn.bijOn e.mapsTo e.symm_mapsTo
+  e.invOn.bijOn e.mapsTo e.mapsTo_symm
 
 protected theorem surjOn : SurjOn e e.source e.target :=
   e.bijOn.surjOn
@@ -455,7 +457,7 @@ theorem symm_image_target_eq_source : e.symm '' e.target = e.source :=
   e.symm.image_source_eq_target
 
 theorem target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source :=
-  e.symm_mapsTo
+  e.mapsTo_symm
 
 /-- Two partial equivs that have the same `source`, same `toFun` and same `invFun`, coincide. -/
 @[ext]
@@ -692,8 +694,8 @@ theorem EqOnSource.target_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.targ
 /-- If two partial equivs are equivalent, so are their inverses. -/
 theorem EqOnSource.symm' {e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm := by
   refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩ <;>
-    simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
-  exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)
+    simp only [symm_source, target_eq h, source_eq h, e'.mapsTo_symm]
+  exact e'.rightInvOn.congr_right e'.mapsTo_symm (source_eq h ▸ h.eqOn.symm)
 
 /-- Two equivalent partial equivs have coinciding inverses on the target. -/
 theorem EqOnSource.symm_eqOn {e e' : PartialEquiv α β} (h : e ≈ e') :
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean b/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean
index fceb69ee60dfa8..0876fd6a970a07 100644
--- a/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean
+++ b/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean
@@ -43,7 +43,7 @@ protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z wher
   open_source := e.open_source
   open_target := e'.open_target
   continuousOn_toFun := e'.continuousOn.comp e.continuousOn <| h ▸ e.mapsTo
-  continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.symm_mapsTo
+  continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.mapsTo_symm
 
 /-- Composing two open partial homeomorphisms, by restricting to the maximal domain where their
 composition is well defined.
@@ -156,8 +156,8 @@ theorem restr_symm_trans {e' : OpenPartialHomeomorph X Y}
     (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (e '' s) := by
   refine ⟨?_, ?_⟩
   · simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
-      PartialEquiv.trans_source, PartialEquiv.symm_source, PartialEquiv.restr_target, coe_coe_symm,
-      PartialEquiv.restr_coe_symm, PartialEquiv.restr_source]
+      PartialEquiv.trans_source, PartialEquiv.symm_source, PartialEquiv.restr_target,
+      coe_toPartialEquiv_symm, PartialEquiv.restr_coe_symm, PartialEquiv.restr_source]
     rw [interior_eq_iff_isOpen.mpr hs', interior_eq_iff_isOpen.mpr hs]
     -- Get rid of the middle term, which is merely distracting.
     rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]
@@ -178,8 +178,8 @@ theorem symm_trans_restr (e' : OpenPartialHomeomorph X Y) (hs : IsOpen s) :
     exact isOpen_image_source_inter e' hs
   refine ⟨?_, ?_⟩
   · simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
-      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_coe_symm, PartialEquiv.restr_source,
-      preimage_inter]
+      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_toPartialEquiv_symm,
+      PartialEquiv.restr_source, preimage_inter]
     -- Shuffle the intersections, pull e'.target into the interior and use interior_inter.
     rw [interior_eq_iff_isOpen.mpr hs,
       ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
index fe67527ca8c151..88c35d0232af2b 100644
--- a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
+++ b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
@@ -201,7 +201,7 @@ def disjointUnion (e e' : OpenPartialHomeomorph X Y) [∀ x, Decidable (x ∈ e.
         (by rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq])
         (by
           rw [e.open_source.inter_frontier_eq]
-          exact eqOn_empty _ _)).replaceEquiv
+          exact eqOn_empty _ _)).replacePartialEquiv
     (e.toPartialEquiv.disjointUnion e'.toPartialEquiv Hs Ht)
     (PartialEquiv.disjointUnion_eq_piecewise _ _ _ _).symm
 
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean b/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
index ba6618af2d38d1..6cebef3c550f9d 100644
--- a/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
+++ b/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
@@ -99,15 +99,19 @@ theorem continuousOn_symm : ContinuousOn e.symm e.target :=
   e.continuousOn_invFun
 
 @[simp, mfld_simps]
-theorem mk_coe (e : PartialEquiv X Y) (a b c d) :
-    (OpenPartialHomeomorph.mk e a b c d : X → Y) = e :=
+theorem coe_mk (e : PartialEquiv X Y) (h₁ h₂ h₃ h₄) :
+    (OpenPartialHomeomorph.mk e h₁ h₂ h₃ h₄ : X → Y) = e :=
   rfl
 
+@[deprecated (since := "2026-05-20")] alias mk_coe := coe_mk
+
 @[simp, mfld_simps]
-theorem mk_coe_symm (e : PartialEquiv X Y) (a b c d) :
-    ((OpenPartialHomeomorph.mk e a b c d).symm : Y → X) = e.symm :=
+theorem coe_mk_symm (e : PartialEquiv X Y) (h₁ h₂ h₃ h₄) :
+    ((OpenPartialHomeomorph.mk e h₁ h₂ h₃ h₄).symm : Y → X) = e.symm :=
   rfl
 
+@[deprecated (since := "2026-05-20")] alias mk_coe_symm := coe_mk_symm
+
 theorem toPartialEquiv_injective :
     Injective (toPartialEquiv : OpenPartialHomeomorph X Y → PartialEquiv X Y)
   | ⟨_, _, _, _, _⟩, ⟨_, _, _, _, _⟩, rfl => rfl
@@ -123,13 +127,17 @@ theorem invFun_eq_coe (e : OpenPartialHomeomorph X Y) : e.invFun = e.symm :=
   rfl
 
 @[simp, mfld_simps]
-theorem coe_coe : (e.toPartialEquiv : X → Y) = e :=
+theorem coe_toPartialEquiv : (e.toPartialEquiv : X → Y) = e :=
   rfl
 
+@[deprecated (since := "2026-05-18")] alias coe_coe := coe_toPartialEquiv
+
 @[simp, mfld_simps]
-theorem coe_coe_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
+theorem coe_toPartialEquiv_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
   rfl
 
+@[deprecated (since := "2026-05-18")] alias coe_coe_symm := coe_toPartialEquiv_symm
+
 @[simp, mfld_simps]
 theorem map_source {x : X} (h : x ∈ e.source) : e x ∈ e.target :=
   e.map_source' h
@@ -156,7 +164,7 @@ theorem eq_symm_apply {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target
 
 protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 
-protected theorem symm_mapsTo : MapsTo e.symm e.target e.source :=
+protected theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
   e.symm.mapsTo
 
 protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv
@@ -170,7 +178,7 @@ protected theorem injOn : InjOn e e.source :=
   e.leftInvOn.injOn
 
 protected theorem bijOn : BijOn e e.source e.target :=
-  e.invOn.bijOn e.mapsTo e.symm_mapsTo
+  e.invOn.bijOn e.mapsTo e.mapsTo_symm
 
 protected theorem surjOn : SurjOn e e.source e.target :=
   e.bijOn.surjOn
@@ -196,7 +204,7 @@ def _root_.Homeomorph.toOpenPartialHomeomorph (e : X ≃ₜ Y) : OpenPartialHome
     by rw [image_univ, e.surjective.range_eq]
 
 /-- Replace `toPartialEquiv` field to provide better definitional equalities. -/
-def replaceEquiv (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y)
+def replacePartialEquiv (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y)
     (h : e.toPartialEquiv = e') : OpenPartialHomeomorph X Y where
   toPartialEquiv := e'
   open_source := h ▸ e.open_source
@@ -204,12 +212,16 @@ def replaceEquiv (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y)
   continuousOn_toFun := h ▸ e.continuousOn_toFun
   continuousOn_invFun := h ▸ e.continuousOn_invFun
 
-theorem replaceEquiv_eq_self (e' : PartialEquiv X Y)
-    (h : e.toPartialEquiv = e') : e.replaceEquiv e' h = e := by
+@[deprecated (since := "2026-05-19")] alias replaceEquiv := replacePartialEquiv
+
+theorem replacePartialEquiv_eq_self (e' : PartialEquiv X Y)
+    (h : e.toPartialEquiv = e') : e.replacePartialEquiv e' h = e := by
   cases e
   subst e'
   rfl
 
+@[deprecated (since := "2026-05-20")] alias replaceEquiv_eq_self := replacePartialEquiv_eq_self
+
 /-- Two open partial homeomorphisms are equal when they have equal `toFun`, `invFun` and `source`.
 It is not sufficient to have equal `toFun` and `source`, as this only determines `invFun` on
 the target. This would only be true for a weaker notion of equality, arguably the right one,