Prove2Me

Lean-Workbook Plus 46600: Trigonometric identity

Proved
WorkbookRestored.plus_46600

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

lean-workbookrestored-importssource-checked

For real x,y,nx,y,n, cos⁡(x−y)−cos⁡(x+y)=n\cos(x-y)-\cos(x+y)=n if and only if 2cos⁡2((x−y)/2)−2cos⁡2((x+y)/2)=n2\cos^2((x-y)/2)-2\cos^2((x+y)/2)=n.

Source: Lean-Workbook row lean_workbook_plus_46600 (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_46600 (x y n : ℝ) : (cos (x - y) - cos (x + y) = n ↔ 2 * cos ((x - y) / 2) ^ 2 - 2 * cos ((x + y) / 2) ^ 2 = n)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_46600; immutable original Prove2Me node 8da09457-cde9-4f70-8315-f0bb70f5c4aa

View graph