Commit 2020-10-15 23:48 3e12a7b9

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.