feat(*): add lemmas about sigma types (#15085)
* move `set.range_sigma_mk` to `data.set.sigma`;
* add `set.preimage_image_sigma_mk_of_ne`, `set.image_sigma_mk_preimage_sigma_map_subset`, and `set.image_sigma_mk_preimage_sigma_map`;
* add `function.injective.of_sigma_map` and `function.injective.sigma_map_iff`;
* don't use pattern matching in the definition of `prod.to_sigma`;
* add `filter.map_sigma_mk_comap`
