lean_workbook_plus_35546Openby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)sinxcosx⋅sinxsinx+cosxsinx⋅cosxcosx=1sin(x)cos(x)\frac{\sin{x}}{\cos{x}} \cdot \frac{\sin{x}}{\sin{x}} + \frac{\cos{x}}{\sin{x}} \cdot \frac{\cos{x}}{\cos{x}} = \frac{1}{\sin(x)\cos(x)}cosxsinx⋅sinxsinx+sinxcosx⋅cosxcosx=sin(x)cos(x)1Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_35546 (x : ℝ) (hx : x ≠ 0) (h : x ≠ π / 2) : (sin x / cos x) * (sin x / sin x) + (cos x / sin x) * (cos x / cos x) = 1 / (sin x * cos x) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph