diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index bbc0360364928..521a5dfa6087f 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -1155,6 +1155,10 @@ def subtypeEquiv {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a,
   right_inv b := Subtype.ext <| by simp
 #align equiv.subtype_equiv Equiv.subtypeEquiv
 
+lemma coe_subtypeEquiv_eq_map {X Y : Type*} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y)
+    (h : ∀ x, p x ↔ q (e x)) : ⇑(e.subtypeEquiv h) = Subtype.map e (h · |>.mp) :=
+  rfl
+
 @[simp]
 theorem subtypeEquiv_refl {p : α → Prop} (h : ∀ a, p a ↔ p (Equiv.refl _ a) := fun a => Iff.rfl) :
     (Equiv.refl α).subtypeEquiv h = Equiv.refl { a : α // p a } := by
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index b4b116bd5828d..8ea4e5f4845d5 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -518,6 +518,26 @@ theorem comp_isOpenMap_iff' (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ h)
   exact hf.comp h.symm.isOpenMap
 #align homeomorph.comp_is_open_map_iff' Homeomorph.comp_isOpenMap_iff'
 
+/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between subtypes corresponding to
+predicates `p : X → Prop` and `q : Y → Prop` so long as `p = q ∘ h`. -/
+@[simps!]
+def subtype {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :
+    {x // p x} ≃ₜ {y // q y} where
+  continuous_toFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using h.continuous.subtype_map _
+  continuous_invFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using
+    h.symm.continuous.subtype_map _
+  __ := h.subtypeEquiv h_iff
+
+@[simp]
+lemma subtype_toEquiv {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :
+    (h.subtype h_iff).toEquiv = h.toEquiv.subtypeEquiv h_iff :=
+  rfl
+
+/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between sets `s : Set X` and `t : Set Y`
+whenever `h` maps `s` onto `t`. -/
+abbrev sets {s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = h ⁻¹' t) : s ≃ₜ t :=
+  h.subtype <| Set.ext_iff.mp h_eq
+
 /-- If two sets are equal, then they are homeomorphic. -/
 def setCongr {s t : Set X} (h : s = t) : s ≃ₜ t where
   continuous_toFun := continuous_inclusion h.subset