Prove2Me

Simplifying a sine expression containing 150 degrees

Proved
WorkbookRestored.plus_1380

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

lean-workbookrestored-importssource-checked

The degree-to-radian conversion gives

2(sin⁡(150π/180)−sin⁡(80π/180))=1−2sin⁡(80π/180).2\bigl(\sin(150\pi/180)-\sin(80\pi/180)\bigr)=1-2\sin(80\pi/180).

Formalization Note This restores source entry lean_workbook_plus_1380 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node 48277d7c-9aeb-489e-9578-2369bb8242c1. This is a separate corrected node because formal statements and preambles are immutable.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Tactic
open Real
Formal statement
theorem WorkbookRestored.plus_1380 (x : ℝ) : 2 * (Real.sin (150 * π / 180) - Real.sin (80 * π / 180)) = 1 - 2 * Real.sin (80 * π / 180)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_1380; original Prove2Me theorem ID 48277d7c-9aeb-489e-9578-2369bb8242c1; Apache-2.0.

View graph