Prove2Me

lean_workbook_plus_74197

Open

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

Given: sin⁡(a+b)=sin⁡acos⁡b+sin⁡bcos⁡a\sin (a + b) = \sin a \cos b + \sin b \cos a Replace aa with aa , and bb with −b-b : sin⁡(a+−b)=sin⁡acos⁡(−b)+sin⁡(−b)cos⁡a\sin (a + -b) = \sin a \cos (-b) + \sin (-b) \cos a Simplify using the unit circle: sin⁡(a−b)=sin⁡acos⁡b−sin⁡bcos⁡a\sin (a - b) = \sin a \cos b - \sin b \cos a

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74197 (a b : ℝ) : sin (a - b) = sin a * cos b - sin b * cos a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph