@[simp]

theorem MeasureTheory.eLpNorm_rclikeOfReal_comp {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] (p : ENNReal) (f : α → ℝ) : eLpNorm (fun (a : α) => ↑(f a)) p μ = eLpNorm f p μ