Derivative of arctangent

Statement

The arctangent is differentiable on $\mathbb{R}$, and $$\frac{d}{dx} \arctan x = \frac{1}{1 + x^2} \quad \text{for every real } x.$$

Remarks

Let $y = \arctan x$. By the inverse function rule and $\tan' = 1 + \tan^2$, the derivative is $\frac{1}{1 + \tan^2 y} = \frac{1}{1 + x^2}$. So $\int_0^1 \frac{dx}{1 + x^2} = \arctan 1 = \frac{\pi}{4}$. Mathlib states it as Real.hasDerivAt_arctan.

Explanations

L1 human

The derivative of the arctangent is the simple rational function $1/(1 + x^2)$. This connects the number $\pi$ with integrals of rational functions.