lean_workbook_plus_386

Proved

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

First equation is $(1+2x-t^2)t-x^2+x+x(2x-t^2)$ \nWhich may be written $(x-t^2+t)(x+t+1)=0$ \nAnd so $x=t^2-t$ or $x=-t-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_386 (x t : ℂ) : (1 + 2 * x - t ^ 2) * t - x ^ 2 + x + x * (2 * x - t ^ 2) = 0 ↔ x = t ^ 2 - t ∨ x = -t - 1   :=  by sorry

Source