case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π

case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π

case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
x : ℂ
hx : x ≠ 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
no goals
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
rw [(ext rfl hi : x = x.re)]
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π

case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π

case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
no goals
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ←
  Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
no goals
case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
exact False.elim (hx (ext hr hi))
no goals
case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
  Real.Angle.coe_zero, zero_add]
no goals
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]