Prove2Me

Completing a square in a sine expression

Proved
WorkbookSource.problem_41598

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

lean-workbooksource-checked

For every real xx,

2(1−2sin⁡2x)+2sin⁡x=94−4(sin⁡x−14)2.2(1-2\sin^2x)+2\sin x=\frac94-4\left(\sin x-\frac14\right)^2.

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

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

View graph