Prove2Me

Lean-Workbook Plus 78015: Trigonometric inequality

Proved
WorkbookRestored.plus_78015

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

lean-workbookrestored-importssource-checked

If 0≤α≤π/20\le\alpha\le\pi/2 and cos⁡α=60/61\cos\alpha=60/61, then sin⁡(α/2)=122/122\sin(\alpha/2)=\sqrt{122}/122.

Source: Lean-Workbook row lean_workbook_plus_78015 (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_78015 (α : ℝ) (h₁ : 0 ≤ α) (h₂ : α ≤ π/2) (h₃ : cos α = 60/61) : sin (α/2) = √122 / 122   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_78015; immutable original Prove2Me node 07451695-0fbf-41d2-93ce-404653489d2f

View graph