x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
simp only [rpow_def, Complex.cpow_def]
no goals
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
split_ifs <;>
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, -IsROrC.ofReal_mul,
(Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]