lean_workbook_plus_51239

Proved

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

Let's say $z = 2$ . Plugging in, we get $f\left(3\cdot (2)\right) = \ f(6)$ right? Which would then be $f\left(\dfrac{6}{3}\right) = \ f(2) = 2^2+2+1 = 7$ . Is that wrong?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51239  (z : ℂ)
  (f : ℂ → ℂ)
  (h₀ : ∀ x, f x = (x / 3)^2 + (x / 3) + 1)
  (h₁ : z = 2) :
  f (3 * z) = 7   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph