feat(data/list/basic): add `list.length_filter_le` and `list.length_filter_map_le` (#15369)
feat(data/list/basic): add `list.length_filter_le` and `list.length_filter_map_le` (#15369)

A `list` can't get longer when applying `list.filter` or `list.filter_map`.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>



Co-authored-by: madvorak <0543540a396ab2ecb2cc41c65788c04d9eb99540@seznam.cz>

leanprover-community/mathlib,leanprover-community/mathlib