Lean golf: Pascal vs. Fibonacci

Question

The Pascal's triangle and the Fibonacci sequence have an interesting connection:

Source: Math is Fun - Pascal's triangle

Your job is to prove this property in Lean theorem prover (Lean 3 + mathlib). Shortest code in bytes wins.

import data.nat.choose.basic
import data.nat.fib
import data.list.defs
import data.list.nat_antidiagonal

theorem X (n : ℕ) :
  ((list.nat.antidiagonal n).map (function.uncurry nat.choose)).sum
  = n.succ.fib :=
sorry -- replace this with actual proof

Since the statement itself depends on the current version of mathlib, it is encouraged to use Lean web editor (as opposed to TIO) to demonstrate that your answer is correct.

Some primer on the built-ins used:

• nat or ℕ is the set/type of natural numbers including zero.
• list.nat.antidiagonal n creates a list of all pairs that sum to n, namely [(0,n), (1,n-1), ..., (n,0)].
• nat.choose n k or n.choose k is equal to \$_nC_k\$.
• nat.fib n or n.fib is the Fibonacci sequence defined with the initial terms of \$f_0 = 0, f_1 = 1\$.

In mathematics notation, the equation to prove is

$$ \forall n \in \mathbb{N},\; \sum^{n}_{i=0}{_iC_{n-i}} = f_{n+1} $$

Rules

• Your code should provide a named theorem or lemma X having the exact type as shown above. Any kind of sidestepping is not allowed.

• The score of your submission is the length of your entire source code in bytes (including the four imports given and any extra imports you need).

Answer 1

Lean, 299 bytes

import data.list data.nat.fib
open nat
def s(n k):=((list.nat.antidiagonal n).map$λa:_×_,choose(a.1+k)a.2).sum
def X:∀n,s n 0=fib(n+1)|0:=rfl|1:=rfl|(n+2):=by{let:∀k,s(n+2)k=choose k(n+2)+s n k+s(n+1)k,induction
n;intro;simp[s,(∘),<-add_one,add_assoc,*]at*;ring,rw[one_add,choose],ring,safe}

Try it on Lean Web Editor

Answer 2

Lean, 247 243 bytes

import data.nat.fib data.list
open nat list.nat
def X:∀n,((antidiagonal n).map$function.uncurry
choose).sum=fib(n+1)|0:=rfl|1:=rfl|(n+2):=by
rw[fib_add_two,antidiagonal_succ_succ'];simpa[<-X,antidiagonal_succ',<-add_assoc,<-list.sum_map_add]

Try it on Lean Web Editor (Note 2/15/2022: this will work within 24 hours)

Perhaps it's cheating, since I contributed very relevant lemmas about antidiagonals to mathlib that were just merged this morning, but I added them for other reasons, I promise! The Lean Web Editor is updated daily, so it should eventually work.