∀ {ι : Type u_1} {αi : ι → Type u_2} {βi : ι → Type u_3} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  ∀ x ∈ Set.univ.pi fun i => (ei i).source, Pi.map (fun i => ↑(ei i).symm) (Pi.map (fun i => ↑(ei i)) x) = x