lean_workbook_plus_25895

Open

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

$cosx-cosy=\frac{1}{5}$ $\implies{-2 \sin \frac{x+y}{2} \sin \frac{x-y}{2}=\frac{1}{5} }$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25895 (x y : ℝ) (h : cos x - cos y = 1 / 5) :
  -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 1 / 5   :=  by sorry

Source