Prove2Me

A numerical instance of the sine subtraction identity

Proved
WorkbookRestored.plus_2039

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

lean-workbookrestored-importssource-checked

For the real sine and cosine functions,

sin⁡30cos⁡10−sin⁡10cos⁡30=sin⁡20.\sin30\cos10-\sin10\cos30=\sin20.

Formalization Note This restores source entry lean_workbook_plus_2039 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 fa5c7b4b-18c4-4181-9392-dbd4ddfaa9bc. 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_2039 : sin 30 * cos 10 - sin 10 * cos 30 = sin 20   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_2039; original Prove2Me theorem ID fa5c7b4b-18c4-4181-9392-dbd4ddfaa9bc; Apache-2.0.

View graph