∀ {α₁ : Type u_4} {β₁ : Type u_5} {γ₁ : Type u_6} [inst : MeasureTheory.MeasureSpace α₁]
  [inst_1 : MeasureTheory.MeasureSpace β₁] [inst_2 : MeasureTheory.MeasureSpace γ₁]
  [MeasureTheory.SFinite MeasureTheory.volume] [MeasureTheory.SFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.prodAssoc) MeasureTheory.volume MeasureTheory.volume