∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : RCLike 𝕜]
  {f : α → 𝕜}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => RCLike.im (f x)) p μ