lean_workbook_plus_43478

Proved

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

Solve the system of equations:\n\n $\left\{\begin{matrix}9x+8y+7z=987 & & & \ 3x+4y+2z=342 & & & \ 2x+5y+8z=258 & & & \end{matrix}\right.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43478 (x y z : ℝ) : (9*x+8*y+7*z=987 ∧ 3*x+4*y+2*z=342 ∧ 2*x+5*y+8*z=258) ↔ x=100 ∧ y=10 ∧ z=1   :=  by sorry

Source