MeasureTheory.hasStrongType_toReal_iff

lemma hasStrongType_toReal_iff {T : (α → ε₁) → (α' → ℝ≥0∞)}    (hT : ∀ f, MemLp f p μ → ∀ᵐ x ∂ν, T f x ≠ ⊤) :    HasStrongType (T · · |>.toReal) p p' μ ν c ↔ HasStrongType T p p' μ ν c := by  refine ⟨fun h ↦ fun f hf ↦ ?_, (·.toReal)⟩  obtain ⟨h1, h2⟩ := h f hf  refine ⟨?_, by rwa [← eLpNorm_toReal_eq (hT f hf)]⟩  rwa [← aestronglyMeasurable_ennreal_toReal_iff]  refine .of_null <| measure_eq_zero_iff_ae_notMem.mpr ?_  filter_upwards [hT f hf] with x hx  simp [hx]