lean_workbook_plus_71216

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_71216    (a b c : ℝ)
    (h₀ : ∀ x ∈ Set.Icc (-1) 1, abs (a * x ^ 2 + b * x + c) ≤ 1) :
    abs a + abs b + abs c ≤ 4   :=  by sorry