APL(NARS), 99 chars

r←f w;h;k
h←0x⋄k←1x
r←h⋄h←k⋄k+←r⋄→2×⍳0≤w-←1

p←{+/{(k-⍵){⍺<⍵-1:0⋄⍵⊃1,⍺!⍨⍳⍺}⍵}¨⍳k←⍵}

c←{∧/{(p⍵)=f⍵}¨⍳⍵}

//43+38+18=99 I know this could be cancelled due the language is different... But how to prove the two computation have the same result in APL?

f is the function for input >=0 that return the fibonacci number, the same the function p that use the Pascal triangle for return the fibonacci number. c is the function that see if the two way of calculate fibonacci number return the same result up the input of c.

  c 10
1
  c 50
1
  c 100
0
  c 100x
1
  c 200x
1
  

note different result because up to some number one has to use big rationals for the approximation errors... ⍵C⍺ of the exercise it would be {⍺<⍵-1:0⋄⍵⊃1,⍺!⍨⍳⍺} but it was need to put ⍺<⍵-1:0 because indexes went out of Pascal triangle, or 90% my error in something.

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.

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