Lean-Workbook Plus 39033: Trigonometric identity

Proved

WorkbookRestored.plus_39033

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

lean-workbookrestored-importssource-checked

For real $x$ and integer $k$ , $\cos x=\pi/2-\sin x+2\pi k$ if and only if $\sin(x+\pi/4)=(4k+1)\pi/(2\sqrt2)$ .

Source: Lean-Workbook row lean_workbook_plus_39033 (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_39033  (x : ℝ) (k : ℤ) :
  (Real.cos x = Real.pi / 2 - Real.sin x + 2 * Real.pi * k) ↔
  (Real.sin (x + Real.pi / 4) = (4 * k + 1) * Real.pi / (2 * Real.sqrt 2))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_39033; immutable original Prove2Me node c702ea8f-f511-4d79-a825-b0aeb40cb865

View graph