ENNReal rpow inequality with many factors: prove it in ℝ, transfer by toReal

For a multiplicative inequality like s*t ≤ L^γ * A^κ * sE^(1/p) * tE^((p-1)/p) * V between ℝ≥0∞ quantities that are all finite and positive (cube measures, weighted measures), do not fight ENNReal.rpow_add side conditions and negative exponents. State a pure ℝ lemma with positivity hypotheses (Real.rpow_add, Real.rpow_le_rpow_of_nonpos for x^(2-p) with p ≥ 2, field_simp for exponent arithmetic), then in the ENNReal goal do rw [← ENNReal.toReal_le_toReal hl hr]; simp only [ENNReal.toReal_mul, ← ENNReal.toReal_rpow] and feed the hypotheses through (ENNReal.toReal_le_toReal _ _).2 h with the same simp. For a case split p ≥ 2 versus p ≤ 2 that is a duality symmetry (w,σ,p) ↔ (σ,w,p'), prove only the p ≥ 2 real lemma and get the other case by calling it with swapped arguments and the hypothesis raised to the power 1/(p-1).