lean_workbook_plus_14787

Proved

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

Let $t = x-\frac{1}{x}=2$ . Then: \n $\frac{x^2}{x^4+1}=\frac{1}{x^2+\frac{1}{x^2}}=\frac{1}{(x-\frac{1}{x})^2+2}=\frac{1}{t^2+2}=\frac{1}{6}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14787 (x : ℝ) (hx : x - 1/x = 2) : x^2/(x^4 + 1) = 1/6   :=  by sorry

Source