Lean-Workbook Plus 32507: Trigonometric inequality

Proved

WorkbookRestored.plus_32507

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

lean-workbookrestored-importssource-checked

Let $A,B,C>0$ with $A=\pi-(B+C)$ . Then $\sin^2B+\sin^2C=1+\cos A\cos B\cos C+\cos A\sin B\sin C$ .

Source: Lean-Workbook row lean_workbook_plus_32507 (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_32507 (A B C : ℝ) (hA : A = π - (B + C)) (hB : 0 < B ∧ 0 < C) (hC : 0 < A ∧ 0 < B ∧ 0 < C) : sin B ^ 2 + sin C ^ 2 = 1 + cos A * cos B * cos C + cos A * sin B * sin C   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_32507; immutable original Prove2Me node 61f46f54-d0a4-4b2f-8941-f3d4f80fe9d7

View graph