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