lean_workbook_plus_30714

Proved

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

hence we get \n\n $x_1=0$ \n\n $x_2=-5$ \n\n $x_3=-2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30714 (x : ℕ → ℝ) (hx : x 1 = 0 ∧ x 2 = -5 ∧ x 3 = -2) : x 1 = 0 ∧ x 2 = -5 ∧ x 3 = -2   :=  by sorry

Source