lean_workbook_plus_42147Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)It suffices to show (j3)+j2=(j+23)\dbinom{j}{3} + j^2 =\dbinom{j+2}{3}(3j)+j2=(3j+2) for all positive integral jjj . Simplifying gives (j3)+j2=16⋅(j−2)(j−1)j+j2=j6((j−1)(j−2)+6j)=j(j2+3j+2)=j(j+1)(j+2)6=(j+23)\dbinom{j}{3} + j^2 = \frac{1}{6} \cdot (j-2)(j-1)j+j^2=\frac{j}{6}((j-1)(j-2) + 6j) = j(j^2+3j+2) = \frac{j(j+1)(j+2)}{6} = \dbinom{j+2}{3}(3j)+j2=61⋅(j−2)(j−1)j+j2=6j((j−1)(j−2)+6j)=j(j2+3j+2)=6j(j+1)(j+2)=(3j+2)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_42147 (j : ℕ) : (j + 2).choose 3 = j.choose 3 + j^2 := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph