Prove2Me

Lean-Workbook Plus 2614: Trigonometric identity

Proved
WorkbookRestored.plus_2614

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

lean-workbookrestored-importssource-checked

If cos⁡(θ−α)=p\cos(\theta - \alpha) = p and sin⁡(θ+β)=q\sin(\theta + \beta) = q then prove that p2+q2−2pqsin⁡(α+β)=cos⁡2(α+β)p^2 + q^2 - 2pq \sin(\alpha + \beta) = \cos^2 (\alpha + \beta)

Source: Lean-Workbook row lean_workbook_plus_2614 (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_2614 (p q α β θ : ℝ) (hp : cos (θ - α) = p) (hq : sin (θ + β) = q) : p^2 + q^2 - 2 * p * q * sin (α + β) = cos (α + β)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_2614; immutable original Prove2Me node 916dfd8a-702c-46f6-8cb9-8703b6d8ebe8

View graph