lean_workbook_plus_69182

Proved

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

Subtract the first equation from the second to get\n\n $x^2+y^2-2xy+4x-4y=5\iff (x-y)^2+4(x-y)-5=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69182 (x y : ℝ) : x^2 + y^2 - 2 * x * y + 4 * x - 4 * y = 5 ↔ (x - y)^2 + 4 * (x - y) - 5 = 0   :=  by sorry

Source