Pythagorean trigonometric identity

Statement

For every real $x$, $$\sin^2 x + \cos^2 x = 1.$$

Remarks

Let $f(x) = \sin^2 x + \cos^2 x$. By the derivatives of sine and cosine, $f'(x) = 2 \sin x \cos x - 2 \cos x \sin x = 0$. So $f$ is constant, and $f(0) = 1$. So $|\sin x| \le 1$ and $|\cos x| \le 1$. Geometrically, the point $(\cos x, \sin x)$ lies on the unit circle. Mathlib states it as Real.sin_sq_add_cos_sq.

Explanations

L1 human

In a right triangle with hypotenuse $1$, the legs are $\cos x$ and $\sin x$. The Pythagorean theorem then says that their squares add up to $1$.