x n : ℂ
⊢ (x ^ n)⁻¹ =
    if arg x = π then if arg x = π then (x ^ n)⁻¹ else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
x n : ℂ
⊢ (x ^ n)⁻¹ = if arg x = π then ↑(starRingEnd ℂ) (x⁻¹ ^ ↑(starRingEnd ℂ) n) else x⁻¹ ^ n
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
case inl
x n : ℂ
h : arg x = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

case inr
x n : ℂ
h : ¬arg x = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
x n : ℂ
⊢ (x ^ n)⁻¹ =
    if arg x = π then if arg x = π then (x ^ n)⁻¹ else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
split_ifs with h
no goals
case inl
x n : ℂ
h : arg x = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹
rfl
no goals
case inr
x n : ℂ
h : ¬arg x = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
rw [inv_cpow _ _ h]