lean_workbook_plus_44218

Proved

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

Prove that $\frac{x^2+1}{x^2-1} = \frac{x}{x+1} + \frac{1}{x-1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44218  (x : ℝ)
  (h₀ : x ≠ 1)
  (h₁ : x ≠ -1) :
  (x^2 + 1) / (x^2 - 1) = x / (x + 1) + 1 / (x - 1)   :=  by sorry

Source