A trigonometric expression as a sum of squares

Proved

WorkbookRestored.plus_271

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

lean-workbookrestored-importssource-checked

For all real $x,y$ ,

1-8\sin x\sin y\cos(x+y)=\bigl(2\cos(x+y)-\cos(x-y)\bigr)^2+\sin^2(x-y).

Formalization Note This restores source entry lean_workbook_plus_271 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node 797bf16b-2aae-4bd0-9282-1643e6163d6c. This is a separate corrected node because formal statements and preambles are immutable.

Preamble

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

Formal statement

theorem WorkbookRestored.plus_271 (x y : ℝ) : (1 - 8 * Real.sin x * Real.sin y * Real.cos (x + y)) = (2 * Real.cos (x + y) - Real.cos (x - y)) ^ 2 + Real.sin (x - y) ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_271; original Prove2Me theorem ID 797bf16b-2aae-4bd0-9282-1643e6163d6c; Apache-2.0.

View graph