Prove2Me

Lean-Workbook Plus 47972: Trigonometric inequality

Proved
WorkbookRestored.plus_47972

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

lean-workbookrestored-importssource-checked

If A,B,C>0A,B,C>0 and A+B+C=πA+B+C=\pi, then 4cos⁡(A/2)cos⁡(B/2)cos⁡(C/2)≥sin⁡(A+B+C)4\cos(A/2)\cos(B/2)\cos(C/2)\ge\sin(A+B+C).

Source: Lean-Workbook row lean_workbook_plus_47972 (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_47972 (A B C : ℝ) (hx: A > 0 ∧ B > 0 ∧ C > 0) (hab : A + B + C = π) : 4 * Real.cos (A / 2) * Real.cos (B / 2) * Real.cos (C / 2) ≥ Real.sin (A + B + C)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_47972; immutable original Prove2Me node ee415506-b41e-4fae-a4b0-b97ef0b535b7

View graph