lean_workbook_plus_54820

Proved

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

Find the integer values of $y$ given $y^2 = x - \frac{x+3}{x^2+1}$ and $x = 2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54820 (x y : ℤ) (hx : x = 2) (h : y^2 = x - (x+3)/(x^2+1)) : y = -1 ∨ y = 1   :=  by sorry

Source