lean_workbook_plus_51872

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_51872 (a b c d : ℝ) (P : ℝ → ℝ) (hP : P = fun x : ℝ => x^4 + a*x^3 + b*x^2 + c*x + d) : P 1 = 827 ∧ P 2 = 1654 ∧ P 3 = 2481 → P 9 + P (-5) = 8012   :=  by sorry