# [Lean], 187 bytes

    def q:list ℕ→bool:=λx,begin
    have A:list ℕ:=begin
    induction x,exact[],apply list.cons 1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,end,exact A=x,end

[Try it online!][TIO-kuemn89o]

[Lean]: https://leanprover.github.io/
[TIO-kuemn89o]: https://tio.run/##ZYxBCoMwEEX3nmKgG6WhoC1dCC48h4jEJG0CIVFMrd2XHqDQ0/QOPYQXSRVFS8owMP/Nm5EMK2spO0EdS9EY6O@v/vEstZZx8nl3qGRnoTyOWwbpYsTJhIWiF2KEVtAh1mFishzhqpI3GM0d0aqBEP1YheBwFYYDBwNiuSG4YQ2YOfN8GtYnPt@agtNguFB0XqZJNya7YS2W4NdZmAfeGpATIxfsh3LQAR2H/oMOilbPfgE "Lean – Try It Online"

A simpler version of this can be found below:
# [Lean], 190 bytes

    def f:ℕ→list ℕ:=λn,begin
    induction n,exact[],apply list.cons 1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,end
    def g:list ℕ→bool:=λx,f(x.length)=x

[Try it online!][TIO-kuemm3e8]

This version defines a helper function `f` which gives the \$n\$th row of pascal's triangle.  From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one.  Instead of doing induction on the length of the list, it just does induction on the list itself.  This turns the already hairy induction into a real mess.

[Lean]: https://leanprover.github.io/
[TIO-kuemm3e8]: https://tio.run/##ZY5NCoMwEIX3nmKgG6VB0JYuBE8iIlGjCYSJkLRN96UHKPQ0vUMP4UXSSH8slmFg3uO94ZOMonMt66DLxvNtvFyl0Ab8meWPO5Ka9QIDge2@MUIhIGGWNqYoCR0GeYIpHTcKNSTkJ1UJDkdhOHAwIL6dhmqmwbw1L1/H/CTka1PxNvINbIOJqs8@PB6tVkpOWJZ0oY0lw97wKLduxQ5UQtgXSRkFsyALmS6NjZ@FtSU7v3/mwkrnnHsC "Lean – Try It Online"