x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else exp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else exp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else exp (log x * y) * 0
    else if x = 0 then if y = 0 then 1 * exp (log x * z) else 0 * exp (log x * z) else exp (log x * y) * exp (log x * z)
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
simp only [cpow_def, ite_mul, boole_mul, mul_ite, mul_boole]
no goals
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else exp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else exp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else exp (log x * y) * 0
    else if x = 0 then if y = 0 then 1 * exp (log x * z) else 0 * exp (log x * z) else exp (log x * y) * exp (log x * z)
simp_all [exp_add, mul_add]