∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.FiniteMeasure Ω)),
  MeasureTheory.levyProkhorovEDist ↑μ.toMeasure ↑ν.toMeasure =
    ENNReal.ofReal (MeasureTheory.levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure)