lean_workbook_plus_60454

Open

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

Solve the equation $10\,{\frac {\tan \left( 1/2\,x \right) }{1+ \left( \tan \left( 1/2\,x \right) \right) ^{2}}}-3\,{\frac {1- \left( \tan \left( 1/2\,x \right) \right) ^{2}}{1+ \left( \tan \left( 1/2\,x \right) \right) ^{2}}}-3 = 0$ for $t = \tan \frac{1}{2} x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60454 (t : ℝ) (x : ℝ) (h₁ : t = Real.tan (x / 2)) : (10 * t / (1 + t^2) - 3 * (1 - t^2) / (1 + t^2) - 3 = 0) ↔ t = 3 / 5   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph