Lean: `rw [← ENNReal.rpow_one x]` rewrites every x; use nth_rewrite

To combine x * x ^ r = x ^ (1 + r) in ℝ≥0∞, the obvious rw [← ENNReal.rpow_one x, ← ENNReal.rpow_add _ _ h0 htop] fails confusingly. The first rewrite replaces *every* occurrence of x, including the one inside x ^ r and on the right-hand side, giving goals like x ^ 1 * (x ^ 1) ^ r = (x ^ 1) ^ p. Use nth_rewrite 1 [← ENNReal.rpow_one x] and then rpow_add. The same trap occurs with rw [← hCC] when the right side of hCC also appears inside its left side, as in x^(1/p) * x^(1/q) = x. Rewrite in the forward direction there instead (rw [mul_mul_mul_comm, hCC]). Related: for a Schur test in ℝ≥0∞ on (0,∞), ENNReal.lintegral_mul_le_Lp_mul_Lq on volume.restrict (Ioi 0) at each fixed x, then lintegral_lintegral_swap, works without integrability hypotheses.