x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ Option.some x ^ y = ↑(x ^ y)
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ ↑x ^ y = ↑(x ^ y)
rw [← ENNReal.some_eq_coe]
no goals
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ (if x = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow x y)) = ↑(NNReal.rpow x y)
simp [h]