x : ℂ
hi : x.im < 0
⊢ arccos ((-x).re / ↑abs (-x)) = -arccos (x.re / ↑abs x) + π
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x + π
rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]
no goals
x : ℂ
hi : x.im < 0
⊢ arccos ((-x).re / ↑abs (-x)) = -arccos (x.re / ↑abs x) + π
simp [neg_div, Real.arccos_neg, add_comm, ← sub_eq_add_neg]