Prove2Me

lean_workbook_plus_80138

Open

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

Prove that 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}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_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

View graph