∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (f : MeasureTheory.SimpleFunc α ENNReal) (c : R),
  f.lintegral (c • μ) = c • f.lintegral μ