∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)), ↑(c • f) = c • ↑f