x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else exp ((if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) * n)) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else exp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else exp (↑(starRingEnd ℂ) (log x) * n)
x n : ℂ
⊢ ↑(starRingEnd ℂ) x ^ n = if arg x = π then x ^ n else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)
simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj,
  log_conj_eq_ite]
no goals
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else exp ((if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) * n)) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else exp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else exp (↑(starRingEnd ℂ) (log x) * n)
split_ifs with hcx hn hx <;> rfl