lean_workbook_plus_80657

Open

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

Find $\cos(2\alpha+2\theta)$ using double angle identities if $\cos(2\alpha) = \frac{7}{25}$ and $\sin(2\alpha) = \frac{24}{25}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80657 (α θ : ℝ) (h₁ : cos (2 * α) = 7 / 25) (h₂ : sin (2 * α) = 24 / 25) : cos (2 * α + 2 * θ) = (7 * cos (2 * θ) - 24 * sin (2 * θ)) / 25   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph