lean_workbook_plus_25208

Open

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

Prove the identity $2\cos{\left(\frac{\pi}{2^{n+1}}\right)} + 2 = 4\cos^2{\left(\frac{\pi}{2^{n+2}}\right)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25208 : ∀ n : ℕ, 2 * Real.cos (π / 2 ^ (n + 1)) + 2 = 4 * (Real.cos (π / 2 ^ (n + 2))) ^ 2   :=  by sorry

Source