lean_workbook_plus_29342
ProvedConsider having to pick objects from a total of . This can be split up into two cases. Either the first object is chosen, or it is not. Now assume the first object is chosen. There are clearly ways to do this. If the first object isn't chosen, there are ways to do this. Another way to count this is to obviously just do . Thus we have that and we are done.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29342 (n r : ℕ) (h₀ : 0 < n ∧ 0 < r) (h₁ : r ≤ n) : Nat.choose n r = Nat.choose (n - 1) (r - 1) + Nat.choose (n - 1) r := by sorry
Source