∀ {α : Type u_1} {ι : Type u_3} {m0 : MeasurableSpace α} [Countable ι] (m : ι → MeasureTheory.Measure α)
  [∀ (n : ι), MeasureTheory.SFinite (m n)], MeasureTheory.SFinite (MeasureTheory.Measure.sum m)