∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : SizeOf α] (posPart negPart : MeasureTheory.Measure α)
  [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] [negPart_finite : MeasureTheory.IsFiniteMeasure negPart]
  (mutuallySingular : posPart.MutuallySingular negPart),
  sizeOf
      { posPart := posPart, negPart := negPart, posPart_finite := posPart_finite, negPart_finite := negPart_finite,
        mutuallySingular := mutuallySingular } =
    1 + sizeOf posPart + sizeOf negPart + sizeOf posPart_finite + sizeOf negPart_finite + sizeOf mutuallySingular