mathlib3

7c2f1663 - chore(analysis/special_functions/trigonometric): review continuity of `tan` (#5429)

chore(analysis/special_functions/trigonometric): review continuity of `tan` (#5429) * prove that `tan` is discontinuous at `x` whenever `cos x = 0`; * turn `continuous_at_tan` and `differentiable_at_tan` into `iff` lemmas; * reformulate various lemmas in terms of `cos x = 0` instead of `∃ k, x = ...`; Co-authored-by: Patrick Massot <patrickmassot@free.fr>