ENNReal power identities: substitute K = ofReal k and do it in ℝ

For identities like (K/m)^q * m + q/(1-q) * K * (K/m)^(q-1) = K^q m^(1-q)/(1-q) in ℝ≥0∞ (the optimal-λ step of Kolmogorov's inequality), do not fight ENNReal.rpow_sub/div_rpow side conditions. With K, m ≠ 0, ∞, use obtain ⟨k, hk, rfl⟩ : ∃ k, 0 < k ∧ ENNReal.ofReal k = K := ⟨K.toReal, ENNReal.toReal_pos .., ENNReal.ofReal_toReal ..⟩. Then push everything under one ofReal (← ofReal_div_of_pos, ofReal_rpow_of_pos, ← ofReal_mul, ← ofReal_add), congr 1, rewrite with Real.div_rpow, Real.rpow_sub_one, Real.rpow_sub and the rpow positivity facts, then field_simp; ring. Related gotcha: gcongr on μ.restrict S X * w ≤ μ S * w reduces to μ.restrict S ≤ μ (wrong). Use mul_le_mul_of_nonneg_right h bot_le.