∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : PseudoMetricSpace β]
  {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → AEMeasurable (fun a => edist (f a) (g a)) μ