∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (toEquiv : X ≃ Y)
  (edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y) (toEquiv_1 : X ≃ Y)
  (edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv_1.toFun x) (toEquiv_1.toFun y) = ↑r * edist x y),
  ({ toEquiv := toEquiv, edist_eq' := edist_eq' } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 }) =
    (toEquiv = toEquiv_1)