Prove2Me

Lean-Workbook Plus 51013: Trigonometric inequality

Proved
WorkbookRestored.plus_51013

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

lean-workbookrestored-importssource-checked

For triangle angles A,B,C>0A,B,C>0 with sum π\pi, (tan⁡(A/2)+tan⁡(B/2)+tan⁡(C/2))2≥3(tan⁡(A/2)tan⁡(B/2)+tan⁡(B/2)tan⁡(C/2)+tan⁡(C/2)tan⁡(A/2))(\tan(A/2)+\tan(B/2)+\tan(C/2))^2\ge3(\tan(A/2)\tan(B/2)+\tan(B/2)\tan(C/2)+\tan(C/2)\tan(A/2)). This is the inequality component of the source.

Source: Lean-Workbook row lean_workbook_plus_51013 (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_51013 :
  ∀ A B C : ℝ, (A + B + C = π ∧ A > 0 ∧ B > 0 ∧ C > 0 → (Real.tan (A / 2) + Real.tan (B / 2) + Real.tan (C / 2))^2 ≥ 3 * (Real.tan (A / 2) * Real.tan (B / 2) + Real.tan (B / 2) * Real.tan (C / 2) + Real.tan (C / 2) * Real.tan (A / 2)))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_51013; immutable original Prove2Me node 9ff5a2ac-e696-48f0-a62a-caf50918ade5

View graph