MeasureTheory.memLorentz_iff_memLorentz_embedRCLike

theorem memLorentz_iff_memLorentz_embedRCLike {𝕂 : Type*} [RCLike 𝕂] {f : α → ℝ≥0} :    MemLorentz (⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f) p q μ ↔ MemLorentz f p q μ := by  constructor  · intro hf    constructor    · have := hf.1      rwa [aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike] at this    · convert hf.2 using 1      apply eLorentzNorm_congr_enorm_ae      apply Eventually.of_forall      intro x      symm      apply enorm_eq_enorm_embedRCLike  · intro hf    constructor    · have := hf.1      rwa [aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike]    · convert hf.2 using 1      apply eLorentzNorm_congr_enorm_ae      apply Eventually.of_forall enorm_eq_enorm_embedRCLike