x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else exp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 then if z = 0 then 1 else 0
    else exp (log (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) * z)
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z
simp only [cpow_def]
no goals
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else exp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 then if z = 0 then 1 else 0
    else exp (log (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) * z)
split_ifs <;> simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]