Prove2Me

lean_workbook_plus_58803

Proved

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

In the first case, p=n−13∧q=n−1  ⟹  f(x)=(x−n+13)(x−n+1)p=n-13\land q=n-1\implies f(x)=(x-n+13)(x-n+1) , thus f(n+1)=14⋅2=28f(n+1)=14\cdot 2=28 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58803  (n p q : ℤ)
  (f : ℤ → ℤ)
  (h₀ : ∀ x, f x = (x - p) * (x - q))
  (h₁ : p = n - 13)
  (h₂ : q = n - 1)
  (h₃ : n + 1 = 15) :
  f (n + 1) = 28   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph