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