mathlib3

637b58e8 - feat(data/finsupp/basic): `alist.lookup` as a finitely supported function (#15443)

feat(data/finsupp/basic): `alist.lookup` as a finitely supported function (#15443) Reworked from #15396. The planned use case for this new definition is to facilitate giving the [Cantor Normal Form](https://leanprover-community.github.io/mathlib_docs/set_theory/ordinal/cantor_normal_form.html#ordinal.CNF) of an ordinal as a finitely supported function. See https://github.com/leanprover-community/mathlib/pull/15396#discussion_r922723604 for further discussion of the motivation.