Prove2Me

An inequality for the sine of a sum

Proved
WorkbookSource.problem_35745

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that (sin⁡(x+y))2≥sin⁡(2x)⋅sin⁡(2y)(\sin(x+y))^2 \ge \sin(2x) \cdot \sin(2y) for all x,yx, y.

Source: InternLM Lean-Workbook, record lean_workbook_35745 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble
import Mathlib
open Real
Formal statement
theorem WorkbookSource.problem_35745 (x y : ℝ) : (sin (x + y))^2 ≥ sin (2*x) * sin (2*y)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_35745; Apache-2.0

View graph