Prove2Me

lean_workbook_plus_36620

Open

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

Prove: sin⁡2θ=2tan⁡θ+cot⁡θ\sin{2\theta}=\frac{2}{\tan{\theta}+\cot{\theta}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36620 (θ : ℝ) : sin (2 * θ) = 2 / (tan θ + 1 / tan θ)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph