lean_workbook_plus_55626Openby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)(sin2x+cos2x)2−2sin2xcos2xsinxcosx=2−sin22xsin2x \frac{(\sin^2 x + \cos^2 x)^2 - 2\sin^2 x \cos^2 x}{\sin x \cos x} = \frac{2 - \sin^2 2x} {\sin 2x}sinxcosx(sin2x+cos2x)2−2sin2xcos2x=sin2x2−sin22xPreambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_55626 : ∀ x : ℝ, ((sin x ^ 2 + cos x ^ 2) ^ 2 - 2 * sin x ^ 2 * cos x ^ 2) / (sin x * cos x) = (2 - sin (2 * x) ^ 2) / sin (2 * x) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph