∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y}
  [inst_2 : (i : X) → Decidable (i ∈ s)] [inst_3 : (i : Y) → Decidable (i ∈ t)],
  e.IsImage s t →
    e'.IsImage s t → Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)