lean_workbook_plus_82040

Proved

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

What is the intersection of the lines given by $2y=-x+3$ and $-y=5x+1$ ? Enter the answer as an ordered pair.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82040 (x y : ℝ) : (2*y = -x + 3 ∧ -y = 5*x + 1) ↔ (x = -5/9 ∧ y = 16/9)   :=  by sorry

Source