case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑x ^ y = ↑(x ^ y)

case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑x ^ y = ↑(x ^ y)
x : ℝ≥0
y : ℝ
h : 0 ≤ y
⊢ ↑x ^ y = ↑(x ^ y)
by_cases hx : x = 0
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑x ^ y = ↑(x ^ y)

case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑x ^ y = ↑(x ^ y)
case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑x ^ y = ↑(x ^ y)
rcases le_iff_eq_or_lt.1 h with (H | H)
no goals
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑x ^ y = ↑(x ^ y)
simp [hx, H.symm]
no goals
case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑x ^ y = ↑(x ^ y)
simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]
no goals
case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑x ^ y = ↑(x ^ y)
exact coe_rpow_of_ne_zero hx _