theorem RCLike.enorm_eq_enorm_embedRCLike {α : Type u_1} {𝕂 : Type u_2} [RCLike 𝕂] {f : α → NNReal} (x : α) : ‖(⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) x‖ₑ = ‖f x‖ₑ

theorem RCLike.aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕂 : Type u_2} [RCLike 𝕂] {f : α → NNReal} : MeasureTheory.AEStronglyMeasurable (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) μ ↔ MeasureTheory.AEStronglyMeasurable f μ