lean_workbook_plus_66230
Open(\sin{x}+\cos{x})^2=\frac{\pi^2}{4^2}\implies\sin{x}\cos{x}=\frac{\pi^2-16}{32}$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66230 (x : ℝ) (hx : (sin x + cos x)^2 = π^2 / 4^2) : sin x * cos x = (π^2 - 16) / 32 := by sorry
Source