AList.lookupFinsupp_apply

theorem AList.lookupFinsupp_apply : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] (l : AList fun _x => M) (a : α), l.lookupFinsupp a = (AList.lookup a l).getD 0

The theorem `AList.lookupFinsupp_apply` states that for any type `α`, another type `M` that has a zero element, and an instance of decidable equality on `α`, given an association list `l` of type `α` to `M` and a value `a` of type `α`, the application of the function `AList.lookupFinsupp` on `l` to `a` is equal to the result of the function `Option.getD` applied to the lookup of `a` in `l` with a default value of zero. In other words, it asserts that looking up a key `a` in the finitely supported function derived from an association list `l` is the same as retrieving the value associated with `a` in `l`, or zero if `a` is not in `l`.

More concisely: For any type `α` with decidable equality, and an association list `l` of type `α` to `M` with a zero element `M`, the application of `AList.lookupFinsupp l a` is equal to `Option.getD (AList.find l a)` or `0`.