{α : Type u_1} →
  [inst : MeasurableSpace α] →
    {β : Type u_2} →
      [inst_1 : MeasurableSpace β] →
        MeasureTheory.ProbabilityMeasure α →
          MeasureTheory.ProbabilityMeasure β → MeasureTheory.ProbabilityMeasure (α × β)