∀ {X : Type u_4} {Y : Type u_5} [inst : PseudoMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : PseudoMetricSpace Y]
  [inst_3 : MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν]
  [IsUnifLocDoublingMeasure μ] [IsUnifLocDoublingMeasure ν], IsUnifLocDoublingMeasure (μ.prod ν)