It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are pattern-matching on the pair (as,bs). The difference is subtle, but since the latter is not an inductive type, this gets Lean's termination checker confused. What you meant to write is probably the following:

def zip {α β : Type} (as: List α) (bs: List β) : List (α × β) :=
    match as, bs with
    | a::arest, b::brest => (a, b) :: zip arest brest
    | _, _ => []

It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are pattern-matching on the pair (as,bs). The difference is subtle, but since the latter is not of the type List of the function's argument, this gets Lean's termination checker confused. What you meant to write is probably the following:

def zip {α β : Type} (as: List α) (bs: List β) : List (α × β) :=
    match as, bs with
    | a::arest, b::brest => (a, b) :: zip arest brest
    | _, _ => []

If you really want to use pairs, then the following is also accepted, but is probably less idiomatic (and has a more complicated termination proof, although in this case Lean still finds it)

def zip {α β : Type} (l: List α × List β) : List (α × β) :=
    match l with
    | (a::arest, b::brest) => (a, b) :: zip (arest,brest)
    | _ => []