Prove2Me

A double-angle value from a sine-cosine sum

Proved
WorkbookSource.problem_14016

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

lean-workbooksource-checked

Given sin⁡x+cos⁡x=65\sin x+\cos x=\tfrac{6}{5}, find sin⁡2x\sin2x.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_14016 (x : ℝ) (h : sin x + cos x = 6/5) : sin (2 * x) = 11/25  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_14016; Apache-2.0

View graph