∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) {x : ↥s},
  ↑x ∈ e.source → ↑e ↑x ∈ (e.subtypeRestr hs).target