x : ℝ≥0
⊢ ↑(↑sqrt x) = ↑(x ^ (1 / 2))
x : ℝ≥0
⊢ ↑sqrt x = x ^ (1 / 2)
refine' NNReal.eq _
x : ℝ≥0
⊢ Real.sqrt ↑x = ↑x ^ (1 / 2)
x : ℝ≥0
⊢ ↑(↑sqrt x) = ↑(x ^ (1 / 2))
push_cast
no goals
x : ℝ≥0
⊢ Real.sqrt ↑x = ↑x ^ (1 / 2)
exact Real.sqrt_eq_rpow x.1