Lean-Workbook Plus 50860: Trigonometric identity

Proved

WorkbookRestored.plus_50860

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 $\cos(x+\pi/4)=(4k+1)\pi/(2\sqrt2)$ .

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

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_50860; immutable original Prove2Me node ae08a050-b812-4c10-bd5c-e545ecb1ceb0

View graph