Prove2Me

Lean-Workbook Plus 80138: Trigonometric identity

Proved
WorkbookRestored.plus_80138

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

lean-workbookrestored-importssource-checked

tan⁡xtan⁡y⋅tan⁡x+tan⁡ytan⁡xtan⁡y−1=tan⁡2xtan⁡y+tan⁡xtan⁡2ytan⁡xtan⁡y−1\tan x \tan y \cdot \frac{\tan x + \tan y}{\tan x \tan y - 1} = \frac{\tan^2 x \tan y + \tan x \tan^2 y}{\tan x \tan y - 1}

Source: Lean-Workbook row lean_workbook_plus_80138 (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_80138  (x y : ℝ) :
  tan x * tan y * (tan x + tan y) / (tan x * tan y - 1) =
    (tan x ^ 2 * tan y + tan x * tan y ^ 2) / (tan x * tan y - 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_80138; immutable original Prove2Me node c876f9bf-d726-4d5e-99ce-d0198fad5f52

View graph