Prove2Me

lean_workbook_plus_58473

Proved

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

P(x,1):f(x+1)=f(x)+1⇒f(x+n)=f(x)+n P(x,1): f(x + 1) = f(x) + 1\Rightarrow f(x + n) = f(x) + n and f(n)=n f(n) = n .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58473 (f : ℕ → ℕ) (x n : ℕ) (h₁ : ∀ x, f (x + 1) = f x + 1) (h₂ : f n = n) : f (x + n) = f x + n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph