{X : Type u_1} →
  {Y : Type u_2} →
    [inst : PseudoEMetricSpace X] →
      [inst_1 : PseudoEMetricSpace Y] →
        (toFun : X → Y) →
          (invFun : Y → X) →
            autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam →
              autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam →
                (∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toFun x) (toFun y) = ↑r * edist x y) → X ≃ᵈ Y