∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {f φ : α → 𝕜}, MeasureTheory.Integrable φ μ → MeasureTheory.MemLp f ⊤ μ → MeasureTheory.Integrable (φ * f) μ