Prove2Me

lean_workbook_plus_65703

Open

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

Given α=(π−(β+γ)) \alpha=(\pi-(\beta+\gamma)) , prove that \n\n sin⁡α=sin⁡(π−(β+γ))=sin⁡π⋅cos⁡(β+γ)−cos⁡π⋅sin⁡(β+γ)=sin⁡(β+γ) \sin \alpha=\sin (\pi-(\beta+\gamma))=\sin \pi \cdot \cos(\beta+\gamma)-\cos \pi \cdot \sin (\beta+\gamma)=\sin (\beta+\gamma)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65703 (α β γ : ℝ) (h : α = π - (β + γ)) : sin α = sin (β + γ)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph