case inl
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

case inr.inr
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
x : ℂ
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
no goals
case inl
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
simp [hi, hi.ne, hi.not_lt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ←
  add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
rw [(ext rfl hi : x = x.re)]
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
no goals
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
simp [hr]
no goals
case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
simp [hr, hi, Real.pi_ne_zero]
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
no goals
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
simp [hr.not_lt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
no goals
case inr.inr
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]