x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if arg x = π then (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ else (exp (log x * n))⁻¹) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (exp (log x * n))⁻¹
x n : ℂ
⊢ x⁻¹ ^ n = if arg x = π then ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul,
  IsROrC.conj_inv, apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg,
  inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
no goals
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if arg x = π then (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ else (exp (log x * n))⁻¹) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (exp (log x * n))⁻¹
split_ifs with hx hn ha ha <;> rfl