∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : DistribSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] (c : 𝕜)
  {f : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ →
    MeasureTheory.SimpleFunc.integral μ (c • f) = c • MeasureTheory.SimpleFunc.integral μ f