lean_workbook_plus_62083

Open

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

Simplify the expression $\cos \alpha \sin \alpha+\sin^{2}\beta = \cos \beta \sin \beta+\sin^{2}\alpha$ given $\alpha+\beta = \frac{\pi}{4}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62083 (α β : ℝ) (h₁ : α + β = π / 4) : cos α * sin α + sin β ^ 2 = cos β * sin β + sin α ^ 2   :=  by sorry

Source