lean_workbook_plus_75435

Proved

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

Solve the system on $\ R$ \n $\ \left\{\begin{matrix} x^4+y^2=\dfrac{697}{81} & \ (x+y)^2-xy-3x-4y+4=0 & \end{matrix}\right.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75435 (x y : ℝ) (h₁ : x^4 + y^2 = 697/81) (h₂ : (x + y)^2 - x*y - 3*x - 4*y + 4 = 0) : x = 2 ∧ y = -1/3   :=  by sorry

Source