mathlib3

079fb166 - feat(analysis/special_functions/complex/arg): `arg_neg` lemmas (#11503)

feat(analysis/special_functions/complex/arg): `arg_neg` lemmas (#11503) Add lemmas about the value of `arg (-x)`: one each for positive and negative sign of `x.im`, two `iff` lemmas saying exactly when it's equal to `arg x - π` or `arg x + π`, and a simpler lemma giving the value of `(arg (-x) : real.angle)` for any nonzero `x`. These replace the previous lemmas `arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg` and `arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg`, which are strictly less general (they have a hypothesis `x.re < 0` that's not needed unless the imaginary part is 0). Those two lemmas are unused in current mathlib (they were used in the proof of `cos_arg` before the golfing in #10365) and it seems reasonable to me to replace them with the more general lemmas.