∀ {α : Type u_1} {m : MeasurableSpace α} (c : ENNReal) (f : MeasureTheory.SimpleFunc α ENNReal)
  (x y : MeasureTheory.Measure α), (c • f).lintegral (x + y) = (c • f).lintegral x + (c • f).lintegral y