# Commit 2020-10-15 23:48 3e12a7b9

View on Github →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.