chore(category_theory): speed-up monoidal.of_has_finite_products

[semorrison]

Just factoring out some proofs, to satisfy the -T 50000 challenge, per #1566.

[fpvandoorn]

LGTM. This doesn't actually speed up the total compilation time, does it?

[semorrison]

I didn’t time it, but I’d suspect you’re correct.

…

On Tue, Oct 29, 2019 at 10:22 mergify[bot] ***@***.***> wrote: Merged #1616 <#1616> into master. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1616?email_source=notifications&email_token=AADUWBDDLY5XXV5MXPGYRN3QQ76G7A5CNFSM4JFMH6W2YY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGOUP7NL6Q#event-2751387130>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AADUWBDLJAZ2JBPLZCAFAJDQQ76G7ANCNFSM4JFMH6WQ> .

[rwbarton]

It probably does increase the amount of work which can be done in parallel, though. Until recently I thought that splitting off Props like this makes no real difference, because Lean can do it automatically. But those examples where by exact made a difference made me realize that my mental model (first the data fields are elaborated, then the properties) is wrong, and all the elaboration is happening on one task. (Probably checking proofs in the kernel happens on separate tasks, but that is usually cheap anyways.)