Choosing two elements from two equal blocks

Proved

WorkbookRestored.plus_14185

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every natural $n$ , $\binom{2n}{2}=2\binom n2+n^2$ .

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_14185 (Apache-2.0).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Factorial.Basic
open Nat

Formal statement

theorem WorkbookRestored.plus_14185 (n : ℕ) : choose (2 * n) 2 = 2 * choose n 2 + n^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_14185; original Prove2Me node c1b512d3-75a7-4d26-99f7-b5599b42c3d3; Apache-2.0

View graph