Prove2Me

Solving a two-equation linear system

Proved
WorkbookSource.problem_40557

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

For real x,yx,y,

(2x+6+2y=0 and 4y+2+2x=0)⟺(x=−5 and y=2).\bigl(2x+6+2y=0\ \text{and}\ 4y+2+2x=0\bigr)\quad\Longleftrightarrow\quad(x=-5\ \text{and}\ y=2).

Source: InternLM Lean-Workbook, record lean_workbook_40557 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_40557 (x y : ℝ) : (2*x+6+2*y=0 ∧ 4*y+2+2*x=0) ↔ (x = -5 ∧ y = 2)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_40557; Apache-2.0

View graph