mathlib3

5ab7eb0f - feat(analysis/special_functions/trigonometric): continuity and differentiability of arctan (#4138)

feat(analysis/special_functions/trigonometric): continuity and differentiability of arctan (#4138) Added lemmas for continuity and differentiability of arctan, as well as various supporting limit lemmas. Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr>