mathlib

1cce6064 - feat(analysis/special_functions/trigonometric): some lemmas (#4638)

feat(analysis/special_functions/trigonometric): some lemmas (#4638) The following changes: - `sin_sub_sin` and friends (sum-to-product lemmas) moved from `trigonometric` to the earlier file `exponential`. (I think the distinction between the files is that `trigonometric` collects the facts that require either differentiation or the definition `pi`, whereas purely algebraic facts about trigonometry go in `exponential`? For example the double-angle formula is in `exponential`). - rewrite proof of `cos_lt_cos_of_nonneg_of_le_pi_div_two` to avoid dependence on `cos_eq_one_iff_of_lt_of_lt` (but not sure if the result is actually simpler, feel free to propose this be reverted) - some new explicit values of trig functions, `cos (π / 3)` and similar - correct a series of lemmas in the `complex` namespace that were stated for real arguments (presumably the author copy-pasted but forgot to rewrite) - lemmas `sin_eq_zero_iff`, `cos_eq_cos_iff`, `sin_eq_sin_iff`