Prove2Me

lean_workbook_plus_2614

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

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)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_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

View graph