lean_workbook_plus_4637

Open

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

$= -\frac{1}{2}\left(\cos{1^2}- \cos{0^2}\right) = \dfrac{1 - \cos{1}}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4637 :
  -(1 / 2) * (Real.cos 1 - Real.cos 0) = (1 - Real.cos 1) / 2   :=  by sorry

Source