Prove2Me

Lean-Workbook Plus 60454: Trigonometric identity

Proved
WorkbookRestored.plus_60454

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Let real t=tan⁡(x/2)t=\tan(x/2). Then 10t/(1+t2)−3(1−t2)/(1+t2)−3=010t/(1+t^2)-3(1-t^2)/(1+t^2)-3=0 if and only if t=3/5t=3/5.

Source: Lean-Workbook row lean_workbook_plus_60454 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
Formal statement
theorem WorkbookRestored.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/blob/main/lean_workbook.json, row lean_workbook_plus_60454; immutable original Prove2Me node 3c45f94b-5e90-4887-add4-d646f04617a4

View graph