∀ {α : Type u_2} {m0 : MeasurableSpace α} {ι : Type u_7} {β : Type u_8} [inst : Fintype ι] {mβ : MeasurableSpace β}
  {m : ι → MeasureTheory.Measure α} {f : α → β},
  AEMeasurable f (∑ i, m i) → MeasureTheory.Measure.map f (∑ i, m i) = ∑ i, MeasureTheory.Measure.map f (m i)