x p : ℝ
hx_pos : 0 < x
⊢ ↑(toNNReal x) ^ p = ↑(toNNReal (x ^ p))
x p : ℝ
hx_pos : 0 < x
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
simp_rw [ENNReal.ofReal]
case h
x p : ℝ
hx_pos : 0 < x
⊢ toNNReal x ≠ 0
x p : ℝ
hx_pos : 0 < x
⊢ ↑(toNNReal x) ^ p = ↑(toNNReal (x ^ p))
rw [coe_rpow_of_ne_zero, coe_eq_coe, Real.toNNReal_rpow_of_nonneg hx_pos.le]
no goals
case h
x p : ℝ
hx_pos : 0 < x
⊢ toNNReal x ≠ 0
simp [hx_pos]