A shifted-angle sine and cosine identity

Proved

WorkbookRestored.plus_162

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

lean-workbookrestored-importssource-checked

For all real $a,b,c$ ,

\cos(a+b)\sin b-\cos(a+c)\sin c=\sin(a+b)\cos b-\sin(a+c)\cos c.

Formalization Note This restores source entry lean_workbook_plus_162 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 4517984b-eb73-4f67-a1df-a9ab9509f558. 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_162  (a b c : ℝ) :
  Real.cos (a + b) * Real.sin b - Real.cos (a + c) * Real.sin c
    = Real.sin (a + b) * Real.cos b - Real.sin (a + c) * Real.cos c   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_162; original Prove2Me theorem ID 4517984b-eb73-4f67-a1df-a9ab9509f558; Apache-2.0.

View graph