Prove2Me

A trigonometric identity using the angle pi over three

Proved
WorkbookSource.problem_19336

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that cos⁡θ+3sin⁡θ=2(cos⁡θcos⁡π3+sin⁡θsin⁡π3) \cos\theta + \sqrt{3}\sin\theta = 2\left(\cos\theta\cos\frac{\pi}{3} + \sin\theta\sin\frac{\pi}{3}\right)

Source: InternLM Lean-Workbook, record lean_workbook_19336 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_19336 : ∀ θ : ℝ, ∃ h : 0 < 3, ∃ h2 : 0 < 2, ∃ h3 : 0 < π, ∃ h4 : 0 < 6, cos θ + Real.sqrt 3 * sin θ = 2 * (cos θ * cos (π / 3) + sin θ * sin (π / 3))  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_19336; Apache-2.0

View graph