[Question]
  [
The Pascal's triangle and the Fibonacci sequence have an interesting connection:
[![enter image description here](https://i.stack.imgur.com/31e0v.png)](https://i.stack.imgur.com/31e0v.png)
*Source: [Math is Fun - Pascal's triangle](https://www.mathsisfun.com/pascals-triangle.html)*
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](https://leanprover-community.github.io/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.](https://codegolf.meta.stackexchange.com/a/23938/78410)
* 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]
# 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](https://leanprover-community.github.io/lean-web-editor/#code=import%20data.list%20data.nat.fib%0Aopen%20nat%0Adef%20s%28n%20k%29%3A%3D%28%28list.nat.antidiagonal%20n%29.map%24%CE%BBa%3A_%C3%97_%2Cchoose%28a.1%2Bk%29a.2%29.sum%0Adef%20X%3A%E2%88%80n%2Cs%20n%200%3Dfib%28n%2B1%29%7C0%3A%3Drfl%7C1%3A%3Drfl%7C%28n%2B2%29%3A%3Dby%7Blet%3A%E2%88%80k%2Cs%28n%2B2%29k%3Dchoose%20k%28n%2B2%29%2Bs%20n%20k%2Bs%28n%2B1%29k%2Cinduction%0An%3Bintro%3Bsimp%5Bs%2C%28%E2%88%98%29%2C%3C-add_one%2Cadd_assoc%2C*%5Dat*%3Bring%2Crw%5Bone_add%2Cchoose%5D%2Cring%2Csafe%7D%0A%0Aexample%20%3A%20%E2%88%80%20%28n%20%3A%20%E2%84%95%29%2C%0A%20%20%28%28list.nat.antidiagonal%20n%29.map%20%28function.uncurry%20nat.choose%29%29.sum%0A%20%20%3D%20n.succ.fib%20%3A%3D%0A%20%20X)
[Answer]
# 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](https://leanprover-community.github.io/lean-web-editor/#code=import%20data.nat.fib%20data.list%0Aopen%20nat%20list.nat%0Adef%20X%3A%E2%88%80n%2C%28%28antidiagonal%20n%29.map%24function.uncurry%0Achoose%29.sum%3Dfib%28n%2B1%29%7C0%3A%3Drfl%7C1%3A%3Drfl%7C%28n%2B2%29%3A%3Dby%0Arw%5Bfib_add_two%2Cantidiagonal_succ_succ%27%5D%3Bsimpa%5B%3C-X%2Cantidiagonal_succ%27%2C%3C-add_assoc%2C%3C-list.sum_map_add%5D) *(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.
]