Prove2Me

Lean-Workbook Plus 74197: Trigonometric identity

Proved
WorkbookRestored.plus_74197

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

lean-workbookrestored-importssource-checked

For real a,ba,b, sin⁡(a−b)=sin⁡acos⁡b−sin⁡bcos⁡a\sin(a-b)=\sin a\cos b-\sin b\cos a.

Source: Lean-Workbook row lean_workbook_plus_74197 (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_74197 (a b : ℝ) : sin (a - b) = sin a * cos b - sin b * cos a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_74197; immutable original Prove2Me node fceb4e5c-7376-4c15-8b23-381b61cd1d6f

View graph