lean_workbook_plus_7551

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Derive the identity $\sin(x)^4+\cos(x)^4=2\, \left( \cos \left( x \right) \right) ^{4}+1-2\, \left( \cos \left( x \right) \right) ^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7551 (x : ℝ) : (sin x)^4 + (cos x)^4 = 2 * (cos x)^4 + 1 - 2 * (cos x)^2   :=  by sorry

Source