Prove2Me

Lean-Workbook Plus 46977: Trigonometric inequality

Proved
WorkbookRestored.plus_46977

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

lean-workbookrestored-importssource-checked

If t=sin⁡x+cos⁡xt=\sin x+\cos x, then sin⁡xcos⁡x=(t2−1)/2\sin x\cos x=(t^2-1)/2 and ∣t∣≤2|t|\le\sqrt2.

Source: Lean-Workbook row lean_workbook_plus_46977 (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_46977 (x : ℝ) (t : ℝ) (ht : t = sin x + cos x) : sin x * cos x = (t^2 - 1) / 2 ∧ |t| ≤ Real.sqrt 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_46977; immutable original Prove2Me node be3ce3b4-1283-4dd7-95ac-c21067b7032e

View graph