lean_workbook_plus_49259
ProvedLet . Then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49259 (a b x y : ℝ) (h₁ : a + b = x) (h₂ : a * b = y) (h₃ : a^2 + b^2 = a + b) : x^2 - 2*y = x := by sorry
Source
Let . Then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49259 (a b x y : ℝ) (h₁ : a + b = x) (h₂ : a * b = y) (h₃ : a^2 + b^2 = a + b) : x^2 - 2*y = x := by sorry