refactor(data/list/count): review API, add lemmas (#16736)
* add `list.countp_join`, `list.countp_map`, `list.countp_mono_left`,
`list.countp_congr`, and `list.count_join`;
* add `@[simp]` attrs to `list.countp_eq_zero`,
`list.countp_eq_length`, `list.count_eq_zero`, and
`list.count_eq_length`;
* golf the proofs of `list.count_bind`, `list.count_map_of_injective`,
and `list.count_le_count_map`.
