Prove2Me

Lean-Workbook Plus 73087: Trigonometric identity

Proved
WorkbookRestored.plus_73087

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

lean-workbookrestored-importssource-checked

For real A,BA,B, sin⁡Acos⁡B=sin⁡Bcos⁡A\sin A\cos B=\sin B\cos A if and only if sin⁡(A−B)=0\sin(A-B)=0.

Source: Lean-Workbook row lean_workbook_plus_73087 (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_73087 :
  ∀ A B : ℝ, (sin A * cos B = sin B * cos A) ↔ sin (A - B) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_73087; immutable original Prove2Me node 67704f6f-4805-4024-8c4b-8daac72dc664

View graph