x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else exp (log ↑x * ↑y)
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y
simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]
no goals
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else exp (log ↑x * ↑y)
split_ifs <;>
simp [Complex.ofReal_log hx]