hopefully fix commit history try 2

scholzhannah · scholzhannah · commit 0b8c5907e99a · 2026-05-19T13:13:11.000+02:00
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -7917,6 +7917,7 @@ public import Mathlib.Topology.Order.T5
 public import Mathlib.Topology.Order.UpperLowerSetTopology
 public import Mathlib.Topology.Order.WithTop
 public import Mathlib.Topology.Partial
+public import Mathlib.Topology.PartialHomeomorph.Defs
 public import Mathlib.Topology.PartitionOfUnity
 public import Mathlib.Topology.Path
 public import Mathlib.Topology.Perfect
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -273,7 +273,7 @@ theorem contMDiffWithinAt_iff_target :
       and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
   simp_rw [cont, ContDiffWithinAtProp, extChartAt, OpenPartialHomeomorph.extend,
     PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe,
-  OpenPartialHomeomorph.coe_toPartialEquiv, modelWithCornersSelf_coe, chartAt_self_eq,
+    OpenPartialHomeomorph.coe_toPartialEquiv, modelWithCornersSelf_coe, chartAt_self_eq,
     OpenPartialHomeomorph.refl_apply, id_comp]
   rfl
 
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
@@ -455,7 +455,7 @@ lemma contMDiff_equivTangentBundleProd_symm :
     filter_upwards [chart_source_mem_nhds (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)]
       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,
+    simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialHomeomorph,
       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
@@ -494,7 +494,7 @@ lemma contMDiff_equivTangentBundleProd_symm :
     filter_upwards [chart_source_mem_nhds (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)]
       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,
+    simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialHomeomorph,
       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
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -751,7 +751,7 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor
     e.prod e' ∈ contDiffGroupoid n (I.prod I') := by
   obtain ⟨he, he_symm⟩ := he
   obtain ⟨he', he'_symm⟩ := he'
-  constructor <;> simp only [PartialEquiv.prod_source, OpenPartialHomeomorph.prod_toPartialEquiv,
+  constructor <;> simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph,
     contDiffPregroupoid]
   · have h3 := ContDiffOn.prodMap he he'
     rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean
@@ -228,7 +228,7 @@ lemma prodMap [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsMani
       (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg)
   · apply IsManifold.mem_maximalAtlas_prod
       (codChart_mem_maximalAtlas hf) (codChart_mem_maximalAtlas hg)
-  · simp only [OpenPartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source,
+  · simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph, PartialEquiv.prod_source,
       preimage_prod_map_prod]
     exact prod_mono hf.source_subset_preimage_source hg.source_subset_preimage_source
   · exact h hf.property hg.property
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
@@ -248,12 +248,13 @@ variable (K)
 
 theorem expMap_source :
     expMap.source = (Set.univ : Set (realSpace K)) := by
-  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
-    Set.pi_univ Set.univ]
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph,
+    PartialEquiv.pi_source, expMap_single, Set.pi_univ Set.univ]
 
 theorem expMap_target :
     expMap.target = Set.univ.pi fun (_ : InfinitePlace K) ↦ Set.Ioi 0 := by
-  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph,
+    PartialEquiv.pi_target, expMap_single]
 
 theorem injective_expMap :
     Function.Injective (expMap : realSpace K → realSpace K) :=
diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -412,8 +412,9 @@ initialize_simps_projections Trivialization (toFun → apply, invFun → symm_ap
 theorem toPretrivialization_injective :
     Function.Injective fun e : Trivialization F proj => e.toPretrivialization := fun e e' h => by
   ext1
-  exacts [OpenPartialHomeomorph.toPartialEquiv_injective
-    (congr_arg Pretrivialization.toPartialEquiv h), congr_arg Pretrivialization.baseSet h]
+  exacts [OpenPartialHomeomorph.toPartialHomeomorph_injective
+    (PartialHomeomorph.toPartialEquiv_injective (congr_arg Pretrivialization.toPartialEquiv h)),
+    congr_arg Pretrivialization.baseSet h]
 
 @[simp, mfld_simps]
 theorem coe_coe : ⇑e.toOpenPartialHomeomorph = e :=
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Basic.lean b/Mathlib/Topology/OpenPartialHomeomorph/Basic.lean
@@ -122,7 +122,7 @@ theorem isOpen_image_iff_of_subset_source {s : Set X} (hs : s ⊆ e.source) :
 
 /-- A `PartialEquiv` with continuous open forward map and open source is a
 `OpenPartialHomeomorph`. -/
-@[simps toPartialEquiv]
+@[simps toPartialHomeomorph]
 def ofContinuousOpenRestrict (e : PartialEquiv X Y) (hc : ContinuousOn e e.source)
     (ho : IsOpenMap (e.source.restrict e)) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y where
   toPartialEquiv := e
@@ -145,7 +145,7 @@ theorem coe_ofContinuousOpenRestrict_symm (e : PartialEquiv X Y) (hc : Continuou
 
 /-- A `PartialEquiv` with continuous open forward map and open source is a
 `OpenPartialHomeomorph`. -/
-@[simps! toPartialEquiv]
+@[simps! toPartialHomeomorph]
 def ofContinuousOpen (e : PartialEquiv X Y) (hc : ContinuousOn e e.source) (ho : IsOpenMap e)
     (hs : IsOpen e.source) : OpenPartialHomeomorph X Y :=
   ofContinuousOpenRestrict e hc (ho.restrict hs) hs
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean b/Mathlib/Topology/OpenPartialHomeomorph/Composition.lean
@@ -37,7 +37,7 @@ variable (e' : OpenPartialHomeomorph Y Z)
 
 /-- Composition of two open partial homeomorphisms when the target of the first and the source of
 the second coincide. -/
-@[simps! apply symm_apply toPartialEquiv, simps! -isSimp source target]
+@[simps! apply symm_apply toPartialHomeomorph, simps! -isSimp source target]
 protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z where
   toPartialEquiv := PartialEquiv.trans' e.toPartialEquiv e'.toPartialEquiv h
   open_source := e.open_source
@@ -99,15 +99,15 @@ theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩
 
 theorem trans_assoc (e'' : OpenPartialHomeomorph Z Z') :
     (e.trans e').trans e'' = e.trans (e'.trans e'') :=
-  toPartialEquiv_injective <| e.1.trans_assoc _ _
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| e.1.trans_assoc _ _
 
 @[simp, mfld_simps]
 theorem trans_refl : e.trans (OpenPartialHomeomorph.refl Y) = e :=
-  toPartialEquiv_injective e.1.trans_refl
+  toPartialHomeomorph_injective (PartialHomeomorph.toPartialEquiv_injective e.1.trans_refl)
 
 @[simp, mfld_simps]
 theorem refl_trans : (OpenPartialHomeomorph.refl X).trans e = e :=
-  toPartialEquiv_injective e.1.refl_trans
+  toPartialHomeomorph_injective (PartialHomeomorph.toPartialEquiv_injective e.1.refl_trans)
 
 theorem trans_ofSet {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e ⁻¹' s) :=
   OpenPartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) <| by
@@ -131,7 +131,7 @@ theorem ofSet_trans_ofSet {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen
   ext <;> simp [hs'.interior_eq]
 
 theorem restr_trans (s : Set X) : (e.restr s).trans e' = (e.trans e').restr s :=
-  toPartialEquiv_injective <|
+  toPartialEquiv_comp_toPartialHomeomorph_injective <|
     PartialEquiv.restr_trans e.toPartialEquiv e'.toPartialEquiv (interior s)
 
 end trans
@@ -197,7 +197,8 @@ variable (e : X ≃ₜ Y) (e' : Y ≃ₜ Z)
 @[simp, mfld_simps]
 theorem trans_toOpenPartialHomeomorph : (e.trans e').toOpenPartialHomeomorph =
     e.toOpenPartialHomeomorph.trans e'.toOpenPartialHomeomorph :=
-  OpenPartialHomeomorph.toPartialEquiv_injective <| Equiv.trans_toPartialEquiv _ _
+  OpenPartialHomeomorph.toPartialHomeomorph_injective <|
+    PartialHomeomorph.toPartialEquiv_injective <| Equiv.trans_toPartialEquiv _ _
 
 /-- Precompose an open partial homeomorphism with a homeomorphism.
 We modify the source and target to have better definitional behavior. -/
@@ -212,7 +213,8 @@ def transOpenPartialHomeomorph (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z)
 
 theorem transOpenPartialHomeomorph_eq_trans (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) :
     e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f' :=
-  OpenPartialHomeomorph.toPartialEquiv_injective <| Equiv.transPartialEquiv_eq_trans _ _
+  OpenPartialHomeomorph.toPartialEquiv_comp_toPartialHomeomorph_injective
+    <| Equiv.transPartialEquiv_eq_trans _ _
 
 @[simp, mfld_simps]
 theorem transOpenPartialHomeomorph_trans (e : X ≃ₜ Y) (f : OpenPartialHomeomorph Y Z)
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
@@ -76,7 +76,7 @@ section Prod
 
 /-- The product of two open partial homeomorphisms, as an open partial homeomorphism on the product
 space. -/
-@[simps! (attr := mfld_simps) -fullyApplied toPartialEquiv apply,
+@[simps! (attr := mfld_simps) -fullyApplied toPartialHomeomorph apply,
   simps! -isSimp source target symm_apply]
 def prod (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') :
     OpenPartialHomeomorph (X × Y) (X' × Y') where
@@ -100,7 +100,7 @@ theorem refl_prod_refl : (OpenPartialHomeomorph.refl X).prod (OpenPartialHomeomo
 theorem prod_trans (e : OpenPartialHomeomorph X Y) (f : OpenPartialHomeomorph Y Z)
     (e' : OpenPartialHomeomorph X' Y') (f' : OpenPartialHomeomorph Y' Z') :
     (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
-  toPartialEquiv_injective <| e.1.prod_trans ..
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| e.1.prod_trans ..
 
 theorem prod_eq_prod_of_nonempty {eX eX' : OpenPartialHomeomorph X X'}
     {eY eY' : OpenPartialHomeomorph Y Y'} (h : (eX.prod eY).source.Nonempty) :
@@ -137,7 +137,7 @@ variable {ι : Type*} [Finite ι] {X Y : ι → Type*} [∀ i, TopologicalSpace
   [∀ i, TopologicalSpace (Y i)] (ei : ∀ i, OpenPartialHomeomorph (X i) (Y i))
 
 /-- The product of a finite family of `OpenPartialHomeomorph`s. -/
-@[simps! toPartialEquiv apply symm_apply source target]
+@[simps! toPartialHomeomorph apply symm_apply source target]
 def pi : OpenPartialHomeomorph (∀ i, X i) (∀ i, Y i) where
   toPartialEquiv := PartialEquiv.pi fun i => (ei i).toPartialEquiv
   open_source := isOpen_set_pi finite_univ fun i _ => (ei i).open_source
@@ -164,7 +164,7 @@ To ensure the maps `toFun` and `invFun` are inverse of each other on the new `so
 the definition assumes that the sets `s` and `t` are related both by `e.is_image` and `e'.is_image`.
 To ensure that the new maps are continuous on `source`/`target`, it also assumes that `e.source` and
 `e'.source` meet `frontier s` on the same set and `e x = e' x` on this intersection. -/
-@[simps! -fullyApplied toPartialEquiv apply]
+@[simps! -fullyApplied toPartialHomeomorph apply]
 def piecewise (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [∀ x, Decidable (x ∈ s)]
     [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
     (Hs : e.source ∩ frontier s = e'.source ∩ frontier s)
@@ -226,7 +226,7 @@ def transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : OpenPart
 
 theorem transHomeomorph_eq_trans (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) :
     e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph :=
-  toPartialEquiv_injective <| PartialEquiv.transEquiv_eq_trans _ _
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.transEquiv_eq_trans _ _
 
 @[simp, mfld_simps]
 theorem transHomeomorph_transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z)
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean b/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
@@ -5,8 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Logic.Equiv.PartialEquiv
-public import Mathlib.Topology.ContinuousOn
+public import Mathlib.Topology.PartialHomeomorph.Defs
 
 /-!
 # Partial homeomorphisms: definitions
@@ -52,11 +51,9 @@ variable {X X' : Type*} {Y Y' : Type*} {Z Z' : Type*}
 
 /-- Partial homeomorphisms, defined on open subsets of the space -/
 structure OpenPartialHomeomorph (X : Type*) (Y : Type*) [TopologicalSpace X]
-    [TopologicalSpace Y] extends PartialEquiv X Y where
+    [TopologicalSpace Y] extends PartialHomeomorph X Y where
   open_source : IsOpen source
   open_target : IsOpen target
-  continuousOn_toFun : ContinuousOn toFun source
-  continuousOn_invFun : ContinuousOn invFun target
 
 namespace OpenPartialHomeomorph
 
@@ -65,8 +62,7 @@ variable (e : OpenPartialHomeomorph X Y)
 /-! Basic properties; inverse (symm instance) -/
 section Basic
 /-- Coercion of an open partial homeomorphisms to a function. We don't use `e.toFun` because it is
-actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.
-While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs. -/
+actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`. -/
 @[coe] def toFun' : X → Y := e.toFun
 
 /-- Coercion of an `OpenPartialHomeomorph` to function.
@@ -77,11 +73,9 @@ instance : CoeFun (OpenPartialHomeomorph X Y) fun _ => X → Y :=
 /-- The inverse of an open partial homeomorphism -/
 @[symm]
 protected def symm : OpenPartialHomeomorph Y X where
-  toPartialEquiv := e.toPartialEquiv.symm
+  toPartialHomeomorph := e.toPartialHomeomorph.symm
   open_source := e.open_target
   open_target := e.open_source
-  continuousOn_toFun := e.continuousOn_invFun
-  continuousOn_invFun := e.continuousOn_toFun
 
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
   because it is a composition of multiple projections. -/
@@ -92,25 +86,32 @@ def Simps.symm_apply (e : OpenPartialHomeomorph X Y) : Y → X := e.symm
 
 initialize_simps_projections OpenPartialHomeomorph (toFun → apply, invFun → symm_apply)
 
+@[fun_prop]
 protected theorem continuousOn : ContinuousOn e e.source :=
   e.continuousOn_toFun
 
+@[fun_prop]
 theorem continuousOn_symm : ContinuousOn e.symm e.target :=
   e.continuousOn_invFun
 
 @[simp, mfld_simps]
 theorem mk_coe (e : PartialEquiv X Y) (h1 h2 h3 h4) :
-    (OpenPartialHomeomorph.mk e h1 h2 h3 h4 : X → Y) = e :=
+    (OpenPartialHomeomorph.mk (.mk e h1 h2) h3 h4 : X → Y) = e :=
   rfl
 
 @[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 :=
+    ((OpenPartialHomeomorph.mk (.mk e a b) c d).symm : Y → X) = e.symm :=
   rfl
 
-theorem toPartialEquiv_injective :
-    Injective (toPartialEquiv : OpenPartialHomeomorph X Y → PartialEquiv X Y)
-  | ⟨_, _, _, _, _⟩, ⟨_, _, _, _, _⟩, rfl => rfl
+theorem toPartialHomeomorph_injective :
+    Injective (toPartialHomeomorph : OpenPartialHomeomorph X Y → PartialHomeomorph X Y)
+  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
+
+theorem toPartialEquiv_comp_toPartialHomeomorph_injective :
+    Injective (PartialHomeomorph.toPartialEquiv ∘ toPartialHomeomorph :
+      OpenPartialHomeomorph X Y → PartialEquiv X Y) :=
+  PartialHomeomorph.toPartialEquiv_injective.comp toPartialHomeomorph_injective
 
 /- Register a few simp lemmas to make sure that `simp` puts the application of a local
 homeomorphism in its normal form, i.e., in terms of its coercion to a function. -/
@@ -138,7 +139,15 @@ theorem coe_toPartialEquiv_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
 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`. -/
+@[simp, mfld_simps]
+theorem coe_toPartialHomeomorph : (e.toPartialHomeomorph : X → Y) = e :=
+  rfl
+
+@[simp, mfld_simps]
+theorem coe_toPartialHomeomorph_symm : (e.toPartialHomeomorph.symm : Y → X) = e.symm :=
+  rfl
+
+/-- Variant of `map_source`, stated in terms of subsets. -/
 lemma map_source'' : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
 
@@ -163,6 +172,8 @@ protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 protected theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
   e.symm.mapsTo
 
+@[deprecated (since := "2026-05-18")] alias symm_mapsTo := OpenPartialHomeomorph.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
@@ -183,15 +194,13 @@ end Basic
 
 /-- Interpret a `Homeomorph` as an `OpenPartialHomeomorph` by restricting it
 to an open set `s` in the domain and to `t` in the codomain. -/
-@[simps! -fullyApplied apply symm_apply toPartialEquiv,
+@[simps! -fullyApplied apply symm_apply toPartialHomeomorph,
   simps! -isSimp source target]
 def _root_.Homeomorph.toOpenPartialHomeomorphOfImageEq (e : X ≃ₜ Y) (s : Set X) (hs : IsOpen s)
     (t : Set Y) (h : e '' s = t) : OpenPartialHomeomorph X Y where
-  toPartialEquiv := e.toPartialEquivOfImageEq s t h
+  toPartialHomeomorph := e.toPartialHomeomorphOfImageEq s t h
   open_source := hs
   open_target := by simpa [← h]
-  continuousOn_toFun := e.continuous.continuousOn
-  continuousOn_invFun := e.symm.continuous.continuousOn
 
 /-- A homeomorphism induces an open partial homeomorphism on the whole space -/
 @[simps! (attr := mfld_simps) -fullyApplied]
@@ -223,7 +232,8 @@ called `EqOnSource`. -/
 @[ext]
 protected theorem ext (e' : OpenPartialHomeomorph X Y) (h : ∀ x, e x = e' x)
     (hinv : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' :=
-  toPartialEquiv_injective (PartialEquiv.ext h hinv hs)
+  toPartialHomeomorph_injective
+    (PartialHomeomorph.ext e.toPartialHomeomorph e'.toPartialHomeomorph h hinv hs)
 
 @[simp, mfld_simps]
 theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm :=
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean b/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean
@@ -171,7 +171,7 @@ theorem isOpen_iff (h : e.IsImage s t) : IsOpen (e.source ∩ s) ↔ IsOpen (e.t
     h.preimage_eq' ▸ e.isOpen_inter_preimage hs⟩
 
 /-- Restrict an `OpenPartialHomeomorph` to a pair of corresponding open sets. -/
-@[simps! -fullyApplied apply symm_apply toPartialEquiv]
+@[simps! -fullyApplied apply symm_apply toPartialHomeomorph]
 def restr (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : OpenPartialHomeomorph X Y where
   toPartialEquiv := h.toPartialEquiv.restr
   open_source := hs
@@ -254,7 +254,7 @@ theorem restr_toPartialEquiv' (s : Set X) (hs : IsOpen s) :
 
 theorem restr_eq_of_source_subset {e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source ⊆ s) :
     e.restr s = e :=
-  toPartialEquiv_injective <| PartialEquiv.restr_eq_of_source_subset <|
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.restr_eq_of_source_subset <|
     interior_maximal h e.open_source
 
 @[simp, mfld_simps]
@@ -315,7 +315,8 @@ theorem eqOnSource_iff (e e' : OpenPartialHomeomorph X Y) :
 
 /-- `EqOnSource` is an equivalence relation. -/
 instance eqOnSourceSetoid : Setoid (OpenPartialHomeomorph X Y) :=
-  { PartialEquiv.eqOnSourceSetoid.comap toPartialEquiv with r := EqOnSource }
+  { PartialEquiv.eqOnSourceSetoid.comap
+    (fun x ↦ (toPartialHomeomorph x).toPartialEquiv) with r := EqOnSource }
 
 theorem eqOnSource_refl : e ≈ e := Setoid.refl _
 
@@ -359,7 +360,7 @@ theorem Set.EqOn.restr_eqOn_source {e e' : OpenPartialHomeomorph X Y}
 
 theorem eq_of_eqOnSource_univ {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') (s : e.source = univ)
     (t : e.target = univ) : e = e' :=
-  toPartialEquiv_injective <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t
 
 variable {s : Set X}
 
diff --git a/Mathlib/Topology/PartialHomeomorph/Defs.lean b/Mathlib/Topology/PartialHomeomorph/Defs.lean
