MeasureTheory.rewrite_norm_func

lemma rewrite_norm_func {q : ℝ} {g : α' → E} [TopologicalSpace E] [ContinuousENorm E]    (hq : 0 < q) {A : ℝ≥0} (hA : 0 < A) (hg : AEStronglyMeasurable g ν) :    ∫⁻ x, ‖g x‖ₑ ^ q ∂ν =    ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ s,    distribution g ((ENNReal.ofReal (2 * A) * s))  ν * s ^ (q - 1) := by  calc  _ = ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ s in Ioi (0 : ℝ),      distribution g ((ENNReal.ofReal (2 * A * s)))  ν * ENNReal.ofReal (s ^ (q - 1)) := by    have : 0 < (A : ℝ) := hA    rw [lintegral_norm_pow_eq_distribution hg (by linarith)]    nth_rewrite 1 [← lintegral_scale_constant_halfspace' (a := (2 * A)) (by linarith)]    rw [← lintegral_const_mul' _ _ (by finiteness), ← lintegral_const_mul' _ _ (by finiteness)]    apply lintegral_congr_ae    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t (zero_lt_t : 0 < t)    nth_rw 12 [mul_comm]    rw [Real.mul_rpow, ← mul_assoc, ← ofReal_mul', ← mul_assoc, ← mul_assoc, ← mul_assoc,        ← ofReal_mul']        <;> try positivity    congr 3    rw [mul_assoc, mul_comm q, ← mul_assoc]    congr 1    rw [abs_of_nonneg] <;> try positivity    nth_rw 1 [← Real.rpow_one (2 * A), ← Real.rpow_add (by linarith), add_sub_cancel]  _ = _ := by    congr 1    rw [lintegral_ennreal_eq_lintegral_Ioi_ofReal]    apply lintegral_congr_ae    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with a ha    rw [ENNReal.ofReal_rpow_of_pos ha, ENNReal.ofReal_mul (by positivity)]