Prove2Me

Choosing a nested pair of subsets

Proved
WorkbookRestored.plus_346

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

lean-workbookrestored-importssource-checked

For natural numbers m≤k≤nm\le k\le n,

(nk)(km)=(nm)(n−mk−m).\binom nk\binom km=\binom nm\binom{n-m}{k-m}.

Formalization Note This restores source entry lean_workbook_plus_346 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node 772ebb0a-ff41-471a-b3be-b37ad0a1b719. This is a separate corrected node because formal statements and preambles are immutable.

Preamble
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic
open Nat
Formal statement
theorem WorkbookRestored.plus_346 (n k m : ℕ) (h₁ : k ≤ n) (h₂ : m ≤ k) : choose n k * choose k m = choose n m * choose (n - m) (k - m)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_346; original Prove2Me theorem ID 772ebb0a-ff41-471a-b3be-b37ad0a1b719; Apache-2.0.

View graph