lean_workbook_plus_34121

Proved

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

Solve equation system\n $x^3+y^2-2=0 \ x^2+y^2+xy-y=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34121 (x y : ℝ) (h₁ : x^3 + y^2 - 2 = 0) (h₂ : x^2 + y^2 + x*y - y = 0) : x = 1 ∧ y = 1   :=  by sorry

Source