Prove2Me

lean_workbook_plus_31177

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Show that sin⁡x+sin⁡y2=sin⁡x+y2cos⁡x−y2≤sin⁡x+y2\frac{\sin x+\sin y}{2}=\sin\frac{x+y}{2}\cos\frac{x-y}{2}\le\sin\frac{x+y}{2} for all x, y∈[0; π]x,\,y\in [0;\,\pi].

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_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

View graph