∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set α) (t : Set β),
  (μ.prod ν) (s ×ˢ t) = μ s * ν t