lean_workbook_plus_39033

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

either $\cos x=\frac{\pi}2-\sin x+2k\pi$ $\iff$ $\sin(x+\frac{\pi}4)=\frac{(4k+1)\pi}{2\sqrt 2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_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

View graph