Prove2Me

Lean-Workbook Plus 62083: Trigonometric identity

Proved
WorkbookRestored.plus_62083

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

lean-workbookrestored-importssource-checked

For real α,β\alpha,\beta with α+β=π/4\alpha+\beta=\pi/4, cos⁡αsin⁡α+sin⁡2β=cos⁡βsin⁡β+sin⁡2α\cos\alpha\sin\alpha+\sin^2\beta=\cos\beta\sin\beta+\sin^2\alpha.

Source: Lean-Workbook row lean_workbook_plus_62083 (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_62083 (α β : ℝ) (h₁ : α + β = π / 4) : cos α * sin α + sin β ^ 2 = cos β * sin β + sin α ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_62083; immutable original Prove2Me node a85dfdf4-c5e8-4dc5-808a-c499f927e9e0

View graph