lean_workbook_plus_19090

Proved

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

If $f(x) = \frac {\left(6x^2 + x + 2\right)^3}{27}$ , then $f(1) = \frac {\left(6 + 1 + 2\right)^3}{27} = \boxed{27}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19090 (f : ℝ → ℝ) (f_def : ∀ x, f x = (6 * x ^ 2 + x + 2) ^ 3 / 27) : f 1 = 27   :=  by sorry

Source