Prove2Me

Lean-Workbook Plus 37185: Trigonometric identity

Proved
WorkbookRestored.plus_37185

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

lean-workbookrestored-importssource-checked

For every real xx, sin⁡2x+sin⁡2(2x)+sin⁡2(3x)+cos⁡2x+cos⁡2(2x)+cos⁡2(3x)=3\sin^2x+\sin^2(2x)+\sin^2(3x)+\cos^2x+\cos^2(2x)+\cos^2(3x)=3.

Source: Lean-Workbook row lean_workbook_plus_37185 (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_37185 : ∀ x : ℝ, (Real.sin x)^2 + (Real.sin (2 * x))^2 + (Real.sin (3 * x))^2 + (Real.cos x)^2 + (Real.cos (2 * x))^2 + (Real.cos (3 * x))^2 = 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_37185; immutable original Prove2Me node 59330872-4cd8-4b47-8f66-d2f966b841da

View graph