∀ {ι : Type u_3} {ι' : Type u_1} [inst : Fintype ι] [inst_1 : Fintype ι'] {Y : ι → Type u_2}
  [inst_2 : (j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (x1 x2 : (i : ι) → Y i),
  edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2