Lean-Workbook Plus 22682: Trigonometric identity

Proved

WorkbookRestored.plus_22682

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Prove that $cos8x=1-32sin^2x+160sin^4x-256sin^6x+128sin^8x$

Source: Lean-Workbook row lean_workbook_plus_22682 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_22682 : ∀ x : ℝ, Real.cos (8 * x) = 1 - 32 * (Real.sin x)^2 + 160 * (Real.sin x)^4 - 256 * (Real.sin x)^6 + 128 * (Real.sin x)^8   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_22682; immutable original Prove2Me node a4274359-af48-4902-a789-ea7b3292deb0

View graph