Lean-Workbook Plus 24283: Trigonometric identity

Proved

WorkbookRestored.plus_24283

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

lean-workbookrestored-importssource-checked

If real $A,B,C$ satisfy $A+B+C=\pi$ , then $\sin^2A+\sin^2B+\sin^2C=2(1+\cos A\cos B\cos C)$ .

Source: Lean-Workbook row lean_workbook_plus_24283 (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_24283 (A B C : ℝ) (hx: A + B + C = π) : (sin A)^2 + (sin B)^2 + (sin C)^2 = 2*(1 + cos A * cos B * cos C)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_24283; immutable original Prove2Me node 5ad05c0c-8aed-4228-b836-edbfe3de6664

View graph