chore: rename {OpenPartialHomeomorph,PartialEquiv}.map_source'' (leanprover-community#40717)

The new name avoids a double prime and also matches the naming convention.
As suggested [here](leanprover-community#39084 (comment)).

Author: scholzhannah

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -275,7 +275,7 @@ theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathCo
     apply e.symm.image_mem_nhds (by simp [e])
     exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht
   · refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_
-    refine e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''
+    refine e.continuousOn_symm.mono <| subset_trans ?_ e.image_source_subset
     exact (pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset
   · exact (image_mono pathComponentIn_subset).trans
       (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -180,9 +180,11 @@ theorem map_source {x : α} (h : x ∈ e.source) : e x ∈ e.target :=
   e.map_source' h
 
 /-- Variant of `e.map_source` and `map_source'`, stated for images of subsets of `source`. -/
-lemma map_source'' : e '' e.source ⊆ e.target :=
+lemma image_source_subset : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
 
+@[deprecated (since := "2026-06-17")] alias map_source'' := image_source_subset
+
 @[simp, mfld_simps]
 theorem map_target {x : β} (h : x ∈ e.target) : e.symm x ∈ e.source :=
   e.map_target' h

Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

@@ -144,9 +144,11 @@ theorem map_source {x : X} (h : x ∈ e.source) : e x ∈ e.target :=
   e.map_source' h
 
 /-- Variant of `map_source`, stated for images of subsets of `source`. -/
-lemma map_source'' : e '' e.source ⊆ e.target :=
+lemma image_source_subset : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
 
+@[deprecated (since := "2026-06-17")] alias map_source'' := image_source_subset
+
 @[simp, mfld_simps]
 theorem map_target {x : Y} (h : x ∈ e.target) : e.symm x ∈ e.source :=
   e.map_target' h