[Merged by Bors] - chore(analysis/special_functions/trigonometric): review continuity of tan

[urkud]

• 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 = ...;

---

• depends on: [Merged by Bors] - chore(analysis/calculus/{fderiv,deriv}): f x ≠ f a for x ≈ a, x ≠ a if ∥z∥ ≤ C * ∥f' z∥ #5420
• depends on: [Merged by Bors] - chore(analysis/special_functions/trigonometric): golf a few more proofs #5423

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - chore(analysis/calculus/{fderiv,deriv}): f x ≠ f a for x ≈ a, x ≠ a if ∥z∥ ≤ C * ∥f' z∥ #5420
• [Merged by Bors] - chore(analysis/special_functions/trigonometric): golf a few more proofs #5423

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[PatrickMassot]

I'm still skeptical that reformulating everything in terms of cos x ≠ 0 is a natural thing to do. It's especially true for lemmas like

tendsto_abs_tan_of_cos_eq_zero {x : ℂ} (hx : cos x = 0) :
  tendsto (λ x, abs (tan x)) (𝓝[{x}ᶜ] x) at_top 

that could be

tendsto_abs_tan_at_top (k : ℤ) :  tendsto (λ x, abs (tan x)) (𝓝[{(2 * k + 1) * π / 2}ᶜ] x) at_top 

that seems pretty clearly less convoluted. But I won't insist on this if you used the lemmas and found it more convenient that way.
bors d+

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[urkud]

I've added tendsto_abs_tan_at_top. My main concerns about formulating lemmas like

lemma continuous_at_tan : continuous_at tan x ↔ ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2 := sorry

are:

1. They're longer.
2. It's not clear why we use (2 * k + 1) * π / 2 and not, e.g., π * k + π / 2, or k * π + π / 2, or π / 2 + π * k.
3. Almost every time lemmas like these were used in special_functions/trigonometric, the first thing to do was to rewrite on cos_eq_zero_iff or cos_ne_zero_iff.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Run tests
• Lint style
• Lint mathlib