Prove2Me

Lean-Workbook Plus 33164: Trigonometric inequality

Proved
WorkbookRestored.plus_33164

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

lean-workbookrestored-importssource-checked

For x∈[0,π]x\in[0,\pi], (1+sin⁡x)cos⁡2x≤32/27(1+\sin x)\cos^2x\le32/27.

Source: Lean-Workbook row lean_workbook_plus_33164 (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_33164 : ∀ x ∈ Set.Icc 0 Real.pi, (1 + Real.sin x) * (Real.cos x)^2 ≤ 32/27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_33164; immutable original Prove2Me node 26b9a448-a92b-45e6-a046-bdbf266c908a

View graph