A proof of the Christmas stocking theorem in Lean

christmas_stocking.lean

import data.nat.choose
import data.finset
import algebra.big_operators.basic

open finset

open_locale big_operators

/- The Christmas stocking theorem:
 - If you start at any point on the edge of the binomial coefficients triangle and 
 - add up the numbers you see in a straight line inwards, the total is equal to the
 - value in the next row down in the other direction.
-/
theorem christmas_stocking {n k : ℕ} : 
∑ i in finset.range (k+1), nat.choose (n+i) i = nat.choose (n+k+1) k :=
begin
  -- Induction on k: we travel k steps into the triangle.
  induction k with k ih,

  -- Base case: effectively, 1 = 1.
  { 
    rw [ add_zero               -- Get rid of +0
       , zero_add
       , nat.choose_zero_right  -- n choose 0 is always 1
       , range_one              -- `range 1` is equivalent to the set {0}
       , sum_singleton          -- summing over a set with one element is just that element
       , nat.choose_zero_right  -- n choose 0 is always 1, again
    ],
  },

  /- Inductive step: 
   - My intuitive way of seeing this is this:
   - We have the following setup:
       n_1
       ⋯
       n_k
       n_(k+1) (n+1)_(k+1)

    - and we've shown n_k = (n+1)_(k+1)
    - Now, we add on n_(k+1) and the total should be (n+1)_(k+2). 
    - But each entry in the triangle is equal to the two entries above it,
    - so (n+1)_(k+2) = n_(k+1) + (n+1)_(k+1), which is what we want!
  -/ 
  rw nat.choose_succ_succ,  -- each entry in the triangle is equal to the two above it.
  repeat {rw nat.add_succ}, -- shift the (+1)s outwards.
  rw ← ih,                  -- apply the inductive hypothesis, to rewrite the RHS as a sum and a binomial term.
  rw add_zero,              -- get rid of +0 that appeared for some reason.
  rw sum_range_succ,        -- separate out the last term of the sum on the LHS
  rw nat.add_succ,          -- shift the (+1) out of that term.
  rw add_comm,              -- now we have the same things on both sides, but in different order, so swap the terms on one side.
  
end