x : ℂ
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
x : ℂ
⊢ arg x⁻¹ = if arg x = π then π else -arg x
rw [← arg_conj, inv_def, mul_comm]
case pos
x : ℂ
hx : x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)

case neg
x : ℂ
hx : ¬x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
x : ℂ
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
by_cases hx : x = 0
no goals
case pos
x : ℂ
hx : x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
simp [hx]
no goals
case neg
x : ℂ
hx : ¬x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
exact arg_real_mul (conj x) (by simp [hx])
no goals
x : ℂ
hx : ¬x = 0
⊢ 0 < (↑normSq x)⁻¹
simp [hx]