lean_workbook_plus_79998

Open

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

Prove that $\sin^4(x) = \frac{3}{8} - \frac{4}{8} \cos(2x) + \frac{1}{8} \cos(4x)$ for all $x$ in the domain of sine.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79998 (x : ℝ) : (sin x)^4 = 3/8 - 4/8 * cos (2 * x) + 1/8 * cos (4 * x)   :=  by sorry

Source