feat(order/filter,*): lemmas about `filter.ne_bot` (#9234)
* add `prod.range_fst`, `prod.range_snd`, `set.range_eval`;
* add `function.surjective_eval`;
* add `filter.*_ne_bot` and/or `filter.*_ne_bot_iff` lemmas for `sup`, `supr`,
`comap prod.fst _`, `comap prod.snd _`, `coprod`, `Coprod`.
