lean_workbook_plus_67605

Proved

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

Tryhard S1From the given, we know that $f(x)=x^2+x+5 \ \forall{x}\in\text{Dom}(f)$ . Hence $f(13)=(13)^2+(13)+5\implies f(13)=\boxed{187}$ as desired.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67605  (f : ℝ → ℝ)
  (h₀ : ∀ x, x ∈ Set.Icc 0 13 → f x = x^2 + x + 5) :
  f 13 = 187   :=  by sorry

Source

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

View graph