Prove2Me

Lean-Workbook Plus 2555: Trigonometric identity

Proved
WorkbookRestored.plus_2555

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

lean-workbookrestored-importssource-checked

Prove that for all reals α\alpha , β\beta and γ\gamma:

sin⁡αsin⁡βsin⁡γsin⁡(α+β+γ)=sin⁡αsin⁡γsin⁡(α+β)sin⁡(β+γ)−sin⁡2αsin⁡2γ\sin\alpha\sin\beta\sin\gamma\sin(\alpha+\beta+\gamma)=\sin\alpha\sin\gamma\sin(\alpha+\beta)\sin(\beta+\gamma)-\sin^2\alpha\sin^2\gamma

Source: Lean-Workbook row lean_workbook_plus_2555 (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_2555 (α β γ : ℝ) :
  sin α * sin β * sin γ * sin (α + β + γ) =
  sin α * sin γ * sin (α + β) * sin (β + γ) -
  sin α ^ 2 * sin γ ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_2555; immutable original Prove2Me node bcfbff16-6634-4ba2-af5b-410093698f16

View graph