← Formalpedia
lean_workbook_plus_2555 Open by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that for all reals α \alpha α β \beta β γ \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 sin α sin β sin γ sin ( α + β + γ ) = sin α sin γ sin ( α + β ) sin ( β + γ ) − sin 2 α sin 2 γ Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_2555 (α β γ : ℝ) :
sin α * sin β * sin γ * sin (α + β + γ) =
sin α * sin γ * sin (α + β) * sin (β + γ) -
sin α ^ 2 * sin γ ^ 2 := by sorry View graph