---
tag: 05P4B4Q22V
kind: statement
role: proposition
name: Derivative of arctangent
msc: [33B10, 26A24]
uses: [065XW2V6C3, 0M0RZ3HSB0, 0SAMR34WXC]
sources:
  - url: https://en.wikipedia.org/wiki/Differentiation_of_trigonometric_functions
    locator: Differentiating the inverse tangent function
---

## 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|0M0RZ3HSB0]] and [[$\tan' = 1 + \tan^2$|0SAMR34WXC]], 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.