x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x) ^ y) = toNNReal x ^ y
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (x ^ y) = toNNReal x ^ y
nth_rw 1 [← Real.coe_toNNReal x hx]
no goals
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x) ^ y) = toNNReal x ^ y
rw [← NNReal.coe_rpow, Real.toNNReal_coe]