Prove2Me

Lean-Workbook Plus 64419: Trigonometric identity

Proved
WorkbookRestored.plus_64419

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

lean-workbookrestored-importssource-checked

cos⁡(a+b)sin⁡(a−b)+cos⁡(b+c)sin⁡(b−c)+cos⁡(c+d)sin⁡(c−d)+cos⁡(d+a)sin⁡(d−a)=0\cos(a+b) \sin(a-b) + \cos (b+c) \sin (b-c) + \cos (c+d) \sin (c-d) + \cos (d+a) \sin (d-a) =0.

Source: Lean-Workbook row lean_workbook_plus_64419 (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_64419 (a b c d : ℝ) : cos (a + b) * sin (a - b) + cos (b + c) * sin (b - c) + cos (c + d) * sin (c - d) + cos (d + a) * sin (d - a) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_64419; immutable original Prove2Me node 21a31ed0-ec16-4f04-a653-a7ff7a6a29a2

View graph