∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E]
  [inst_4 : NormedSpace ℝ E] [SMulCommClass ℝ 𝕜 E] (c : 𝕜) (f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)),
  MeasureTheory.L1.SimpleFunc.integral (c • f) = c • MeasureTheory.L1.SimpleFunc.integral f