Prove2Me

Lean-Workbook Plus 31177: Trigonometric inequality

Proved
WorkbookRestored.plus_31177

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

lean-workbookrestored-importssource-checked

For x,y∈[0,π]x,y\in[0,\pi], sin⁡((x+y)/2)cos⁡((x−y)/2)≤sin⁡((x+y)/2)\sin((x+y)/2)\cos((x-y)/2)\le\sin((x+y)/2). This is the inequality component of the source’s sum-to-product statement.

Source: Lean-Workbook row lean_workbook_plus_31177 (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_31177 (x y : ℝ) (hx : 0 ≤ x ∧ x ≤ π) (hy : 0 ≤ y ∧ y ≤ π) :
  sin ((x + y) / 2) * cos ((x - y) / 2) ≤ sin ((x + y) / 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_31177; immutable original Prove2Me node 06d3a222-d5f5-452d-8975-70af7c7f723f

View graph