mathlib

3e12a7b9 - chore(category_theory/limits/binary_products): fixup binary product lemmas (#4376)

chore(category_theory/limits/binary_products): fixup binary product lemmas (#4376) The main changes in here are: - `prod.map` is now a def, not an abbreviation. I think this is an important change because oftentimes `simp` will reduce it to `lim.map` and then get stuck, which is tough to debug and usually the wrong step to take. Instead, the `prod.map_fst` and `snd` lemmas are proved directly rather than with simp, and these are used to get everything else. - I added a couple of new simp lemmas and rewrote a few others: the overall guide here is that more things can be proved by `rw` or `simp` *without using ext*. The idea of this is that when you're dealing with a chain of compositions containing product morphisms, it's much nicer to be able to rewrite (or simp) the parts you want rather than needing to do an auxiliary `have` and use `ext` in there, then rewrite using this lemma inside your big chain. In this file at least I managed to get rid of a bunch of uses of `ext` (and also convert `tidy` to `simp`) so I'm pretty sure these changes were positive. - Moved around some definitions and lemmas. No big changes here, mostly just putting things which work similarly closer. - Weakened typeclass assumptions: in particular for `prod_comparison`. - Renamed some `prod_` lemmas to `prod.`, since there used to be a mix between the two; so I've made the usage consistent. + dual versions of all the above.