diff --git a/Mathlib.lean b/Mathlib.lean
index 57d9493e5cebd8..eb895e155b9637 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -8034,6 +8034,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/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
index fe370981f4d96c..d5747cf0dbe93d 100644
--- 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
index 79619e7d1384c9..11fbcf447b60bd 100644
--- 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/LocalDiffeomorph.lean b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
index 6edbe4e85b53d5..db32ceb65a874e 100644
--- a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
+++ b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
@@ -105,7 +105,7 @@ namespace PartialDiffeomorph
 variable (Φ : PartialDiffeomorph I J M N n)
 
 /-- A partial diffeomorphism is also a local homeomorphism. -/
-@[expose, simps toPartialEquiv]
+@[expose, simps toPartialHomeomorph_toPartialEquiv]
 def toOpenPartialHomeomorph : OpenPartialHomeomorph M N where
   toPartialEquiv := Φ.toPartialEquiv
   open_source := Φ.open_source
diff --git a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean
index eba67d29639cd2..ab1e4a4b92d4d4 100644
--- a/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean
+++ b/Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean
@@ -238,7 +238,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
index f3b6b6f2488b12..7da4f53aa81781 100644
--- 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
index a3b14ce26719a8..38133c78000fab 100644
--- a/Mathlib/Topology/FiberBundle/Trivialization.lean
+++ b/Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -412,8 +412,8 @@ 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.toPartialEquiv_injective congr(Pretrivialization.toPartialEquiv $h),
+    congr(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
index d7b7543fc806ee..bb87598e2874a5 100644
--- 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
index 943cdfd79060bf..b60b59954a009f 100644
--- 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
@@ -103,11 +103,11 @@ theorem trans_assoc (e'' : OpenPartialHomeomorph Z Z') :
 
 @[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
@@ -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. -/
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
index b1543e614aa23f..7da001d1a1cebe 100644
--- 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
@@ -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]
+@[simps! toPartialHomeomorph apply symm_apply]
 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)
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean b/Mathlib/Topology/OpenPartialHomeomorph/Defs.lean
index 362cbe712da3c6..a8f90bd94cf6df 100644
--- 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
@@ -17,7 +16,7 @@ This file defines homeomorphisms between open subsets of topological spaces. An
 Additionally, we require that these sets are open, and that the functions are continuous on them.
 Equivalently, they are homeomorphisms there.
 
-As in equivs, we register a coercion to functions, and we use `e x` and `e.symm x` throughout
+As for `Equiv`s, we register a coercion to functions, and we use `e x` and `e.symm x` throughout
 instead of `e.toFun x` and `e.invFun x`.
 
 ## Main 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. -/
@@ -100,21 +94,25 @@ theorem continuousOn_symm : ContinuousOn e.symm e.target :=
 
 @[simp, mfld_simps]
 theorem coe_mk (e : PartialEquiv X Y) (h₁ h₂ h₃ h₄) :
-    (OpenPartialHomeomorph.mk e h₁ h₂ h₃ h₄ : X → Y) = e :=
+    (OpenPartialHomeomorph.mk (.mk e h₁ h₂) h₃ h₄ : X → Y) = e :=
   rfl
 
 @[deprecated (since := "2026-05-20")] alias mk_coe := coe_mk
 
 @[simp, mfld_simps]
 theorem coe_mk_symm (e : PartialEquiv X Y) (h₁ h₂ h₃ h₄) :
-    ((OpenPartialHomeomorph.mk e h₁ h₂ h₃ h₄).symm : Y → X) = e.symm :=
+    ((OpenPartialHomeomorph.mk (.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 toPartialHomeomorph_injective :
+    Injective (toPartialHomeomorph : OpenPartialHomeomorph X Y → PartialHomeomorph X Y)
+  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
+
 theorem toPartialEquiv_injective :
-    Injective (toPartialEquiv : OpenPartialHomeomorph X Y → PartialEquiv X Y)
-  | ⟨_, _, _, _, _⟩, ⟨_, _, _, _, _⟩, rfl => rfl
+    Injective (fun f ↦ f.toPartialEquiv : 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. -/
@@ -143,6 +141,14 @@ 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
 
+@[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 for images of subsets of `source`. -/
 lemma image_source_subset : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
@@ -192,15 +198,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]
@@ -211,11 +215,9 @@ def _root_.Homeomorph.toOpenPartialHomeomorph (e : X ≃ₜ Y) : OpenPartialHome
 /-- Replace `toPartialEquiv` field to provide better definitional equalities. -/
 def replacePartialEquiv (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y)
     (h : e.toPartialEquiv = e') : OpenPartialHomeomorph X Y where
-  toPartialEquiv := e'
+  toPartialHomeomorph := e.toPartialHomeomorph.replacePartialEquiv e' h
   open_source := h ▸ e.open_source
   open_target := h ▸ e.open_target
-  continuousOn_toFun := h ▸ e.continuousOn_toFun
-  continuousOn_invFun := h ▸ e.continuousOn_invFun
 
 @[deprecated (since := "2026-05-19")] alias replaceEquiv := replacePartialEquiv
 
@@ -234,7 +236,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
index 4046c9bec712cd..fe21e40169ee0f 100644
--- 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
@@ -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 _
 
diff --git a/Mathlib/Topology/PartialHomeomorph/Defs.lean b/Mathlib/Topology/PartialHomeomorph/Defs.lean
new file mode 100644
index 00000000000000..ab78f5be70780c
--- /dev/null
+++ b/Mathlib/Topology/PartialHomeomorph/Defs.lean
@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+module
+
+public import Mathlib.Logic.Equiv.PartialEquiv
+public import Mathlib.Topology.ContinuousOn
+
+/-!
+# Partial homeomorphisms: definitions
+
+This file defines homeomorphisms between subsets of topological spaces. An element `e` of
+`PartialHomeomorph X Y` is an extension of `PartialEquiv X Y`, i.e., it is a pair of functions
+`e.toFun` and `e.invFun`, inverse of each other on the sets `e.source` and `e.target`.
+Additionally, we require that the functions are continuous on them. Equivalently, they are
+homeomorphisms there.
+
+As for `Equiv`s, we register a coercion to functions, and we use `e x` and `e.symm x` throughout
+instead of `e.toFun x` and `e.invFun x`.
+
+## Main definitions
+
+This file is intentionally kept small; many other constructions of, and lemmas about,
+partial homeomorphisms can be found in other files under `Mathlib/Topology/PartialHomeomorph/`.
+
+* `Homeomorph.toPartialHomeomorph`: associating a partial homeomorphism to a
+  homeomorphism, with `source = target = Set.univ`;
+* `PartialHomeomorph.symm`: the inverse of a partial homeomorphism
+
+## Implementation notes
+
+Most statements are copied from their `PartialEquiv` versions, although some care is required.
+
+For design notes, see `PartialEquiv.lean`.
+
+### Local coding conventions
+
+If a lemma deals with the intersection of a set with either source or target of a `PartialEquiv`,
+then it should use `e.source ∩ s` or `e.target ∩ t`, not `s ∩ e.source` or `t ∩ e.target`.
+-/
+
+@[expose] public section
+
+open Function Set Filter Topology
+
+variable {X X' : Type*} {Y Y' : Type*} {Z Z' : Type*}
+  [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y']
+  [TopologicalSpace Z] [TopologicalSpace Z']
+
+/-- Partial homeomorphisms, defined on subsets of the space -/
+structure PartialHomeomorph (X : Type*) (Y : Type*) [TopologicalSpace X]
+    [TopologicalSpace Y] extends PartialEquiv X Y where
+  continuousOn_toFun : ContinuousOn toFun source
+  continuousOn_invFun : ContinuousOn invFun target
+
+namespace PartialHomeomorph
+
+variable (e : PartialHomeomorph X Y)
+
+/-! Basic properties; inverse (symm instance) -/
+section Basic
+/-- Coercion of a 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`. -/
+@[coe] def toFun' : X → Y := e.toFun
+
+/-- Coercion of a `PartialHomeomorph` to function.
+Note that a `PartialHomeomorph` is not `DFunLike`. -/
+instance : CoeFun (PartialHomeomorph X Y) fun _ => X → Y :=
+  ⟨fun e => e.toFun'⟩
+
+/-- The inverse of a partial homeomorphism -/
+@[symm]
+protected def symm : PartialHomeomorph Y X where
+  toPartialEquiv := e.toPartialEquiv.symm
+  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. -/
+def Simps.apply (e : PartialHomeomorph X Y) : X → Y := e
+
+/-- See Note [custom simps projection] -/
+def Simps.symm_apply (e : PartialHomeomorph X Y) : Y → X := e.symm
+
+initialize_simps_projections PartialHomeomorph (toFun → apply, invFun → symm_apply)
+
+protected theorem continuousOn : ContinuousOn e e.source :=
+  e.continuousOn_toFun
+
+theorem continuousOn_symm : ContinuousOn e.symm e.target :=
+  e.continuousOn_invFun
+
+@[simp]
+theorem coe_mk (e : PartialEquiv X Y) (h₁ h₂) : (PartialHomeomorph.mk e h₁ h₂ : X → Y) = e := rfl
+
+@[simp]
+theorem coe_mk_symm (e : PartialEquiv X Y) (h₁ h₂) :
+    ((PartialHomeomorph.mk e h₁ h₂).symm : Y → X) = e.symm :=
+  rfl
+
+theorem toPartialEquiv_injective :
+    Injective (toPartialEquiv : PartialHomeomorph X Y → PartialEquiv X Y)
+  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
+
+/- 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. -/
+@[simp]
+theorem toFun_eq_coe (e : PartialHomeomorph X Y) : e.toFun = e :=
+  rfl
+
+@[simp]
+theorem invFun_eq_coe (e : PartialHomeomorph X Y) : e.invFun = e.symm :=
+  rfl
+
+@[simp]
+theorem coe_toPartialEquiv : (e.toPartialEquiv : X → Y) = e :=
+  rfl
+
+@[simp]
+theorem coe_toPartialEquiv_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
+  rfl
+
+@[simp]
+theorem map_source {x : X} (h : x ∈ e.source) : e x ∈ e.target :=
+  e.map_source' h
+
+/-- Variant of `map_source`, stated in terms of subsets. -/
+lemma image_source_subset : e '' e.source ⊆ e.target :=
+  fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
+
+@[simp]
+theorem map_target {x : Y} (h : x ∈ e.target) : e.symm x ∈ e.source :=
+  e.map_target' h
+
+@[simp]
+theorem left_inv {x : X} (h : x ∈ e.source) : e.symm (e x) = x :=
+  e.left_inv' h
+
+@[simp]
+theorem right_inv {x : Y} (h : x ∈ e.target) : e (e.symm x) = x :=
+  e.right_inv' h
+
+theorem eq_symm_apply {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target) :
+    x = e.symm y ↔ e x = y :=
+  e.toPartialEquiv.eq_symm_apply hx hy
+
+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
+
+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
+
+protected theorem invOn : InvOn e.symm e e.source e.target :=
+  ⟨e.leftInvOn, e.rightInvOn⟩
+
+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.mapsTo_symm
+
+protected theorem surjOn : SurjOn e e.source e.target :=
+  e.bijOn.surjOn
+
+end Basic
+
+/-- Interpret a `Homeomorph` as a `PartialHomeomorph` by restricting it
+to a set `s` in the domain and to `t` in the codomain. -/
+@[simps! -fullyApplied apply symm_apply toPartialEquiv,
+  simps! -isSimp source target]
+def _root_.Homeomorph.toPartialHomeomorphOfImageEq (e : X ≃ₜ Y) (s : Set X)
+    (t : Set Y) (h : e '' s = t) : PartialHomeomorph X Y where
+  toPartialEquiv := e.toPartialEquivOfImageEq s t h
+  continuousOn_toFun := e.continuous.continuousOn
+  continuousOn_invFun := e.symm.continuous.continuousOn
+
+/-- A homeomorphism induces a partial homeomorphism on the whole space -/
+@[simps! -fullyApplied]
+def _root_.Homeomorph.toPartialHomeomorph (e : X ≃ₜ Y) : PartialHomeomorph X Y :=
+  e.toPartialHomeomorphOfImageEq univ univ <| by rw [image_univ, e.surjective.range_eq]
+
+/-- Replace `toPartialEquiv` field to provide better definitional equalities. -/
+def replacePartialEquiv (e : PartialHomeomorph X Y) (e' : PartialEquiv X Y)
+    (h : e.toPartialEquiv = e') : PartialHomeomorph X Y where
+  toPartialEquiv := e'
+  continuousOn_toFun := h ▸ e.continuousOn_toFun
+  continuousOn_invFun := h ▸ e.continuousOn_invFun
+
+theorem replacePartialEquiv_eq_self (e' : PartialEquiv X Y)
+    (h : e.toPartialEquiv = e') : e.replacePartialEquiv e' h = e := by
+  cases e
+  subst e'
+  rfl
+
+/-- Two 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,
+called `EqOnSource`. -/
+@[ext]
+protected theorem ext (e' : PartialHomeomorph 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)
+
+@[simp]
+theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm :=
+  rfl
+
+-- The following lemmas are already simp via `PartialEquiv`
+theorem symm_source : e.symm.source = e.target :=
+  rfl
+
+theorem symm_target : e.symm.target = e.source :=
+  rfl
+
+@[simp] theorem symm_symm : e.symm.symm = e := rfl
+
+theorem symm_bijective : Function.Bijective
+    (PartialHomeomorph.symm : PartialHomeomorph X Y → PartialHomeomorph Y X) :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
+end PartialHomeomorph