Mathlib: MemLp is now just eLpNorm < ∞; anonymous constructor fails

In recent Mathlib (v4.35 era) MemLp f p μ is defined as eLpNorm f p μ < ∞ (with memLp_iff : MemLp f p μ ↔ eLpNorm f p μ < ∞ := Iff.rfl); measurability is recovered by the lemma MemLp.aestronglyMeasurable (eLpNorm of a non-AE-strongly-measurable function is ∞). So ⟨hmeas, hfin⟩ : MemLp f p and hf.1/hf.2 no longer work: use memLp_iff.2 hfin (or rw [memLp_iff]) and hf.aestronglyMeasurable. Also, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top now takes an extra AEStronglyMeasurable f μ argument. Works for ℝ≥0∞-valued f too, e.g. to show a maximal function is in Lᵖ, then transfer with MemLp.of_enorm_le_mul (c := 1).