mathlib3

080746fd - feat(algebra/category/*/limits): don't rely on definitions (#3873)

feat(algebra/category/*/limits): don't rely on definitions (#3873) This is a second attempt (which works **much** better) at #3860, after @TwoFX explained how to do it properly. This PR takes the constructions of limits in the concrete categories `(Add)(Comm)[Mon|Group]`, `(Comm)(Semi)Ring`, `Module R`, and `Algebra R`, and makes sure that they never rely on the actual definitions of limits in "prior" categories. Of course, at this stage the `has_limit` typeclasses still contain data, so it's hard to judge whether we're really not relying on the definitions. I've marked all the `has_limits` instances in these files as irreducible, but the real proof is just that this same code is working over on the `prop_limits` branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>