Prove2Me

Lean-Workbook Plus 15035: Trigonometric identity

Proved
WorkbookRestored.plus_15035

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

If 2sin⁡2θ=5/72\sin^2\theta=5/7, then sin⁡2(2θ)=45/49\sin^2(2\theta)=45/49.

Source: Lean-Workbook row lean_workbook_plus_15035 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_15035 (θ : ℝ) (h : 2 * sin θ ^ 2 = 5/7) : sin (2 * θ) ^ 2 = 45/49   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_15035; immutable original Prove2Me node 66a80e0e-c405-4afa-bcd7-fe7ee7cb73c7

View graph