lean_workbook_plus_47559

Proved

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

Plugging $y=x-3$ into the second equation we get $-2(x-3)=2(x^2+1)\iff x^2+x-2=0\iff x\in\{-2,1\}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47559  (x y : ℝ)
  (h₀ : y = x - 3)
  (h₁ : -2 * y = 2 * (x^2 + 1)) :
  x = -2 ∨ x = 1   :=  by sorry

Source