∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s),
  (OpenPartialHomeomorph.ofSet s hs).trans e = e.restr (e.source ∩ s)