Prove2Me

Lean-Workbook Plus 33683: Trigonometric inequality

Proved
WorkbookRestored.plus_33683

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

lean-workbookrestored-importssource-checked

For real A,B,CA,B,C, (sin⁡A+sin⁡B+sin⁡C)2≤3(sin⁡2A+sin⁡2B+sin⁡2C)(\sin A+\sin B+\sin C)^2\le3(\sin^2A+\sin^2B+\sin^2C).

Source: Lean-Workbook row lean_workbook_plus_33683 (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_33683 (A B C : ℝ) : (sin A + sin B + sin C) ^ 2 ≤ 3 * (sin A ^ 2 + sin B ^ 2 + sin C ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_33683; immutable original Prove2Me node 0ac4fb6d-d8eb-4817-95e5-b5e160592ff7

View graph