Derivative of tangent

Statement

The tangent function is differentiable at every $x$ with $\cos x \ne 0$, and $$\tan'(x) = \frac{1}{\cos^2 x} = 1 + \tan^2 x.$$

Remarks

The quotient rule gives $\tan' = \frac{\cos \cdot \cos - \sin \cdot (-\sin)}{\cos^2}$. The Pythagorean identity turns the numerator into $1$. The derivative is positive. So $\tan$ is strictly increasing on $(-\pi/2, \pi/2)$. Mathlib states it as Real.hasDerivAt_tan.

Explanations

L1 human

The tangent function always rises, and it rises faster and faster near its asymptotes. Its slope at $0$ is $1$.