[Merged by Bors] - perf(topology/sheaves/presheaf_of_functions): speedups

[alreadydone]

Speed upCommRing_yoneda (which caused a bors failure) from >20s to <2.5s by filling in automatic fields. (merged in another PR)

Speed up presheaf_to_Types from 13.3s to 0.3s and presheaf_to_Type from 4s to 0.1s by filling in automatic fields.

---

Zulip

[alreadydone]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[kbuzzard]

Thanks! This declaration was causing unrelated timeouts in several other places (e.g. #13250 and #16721)

[semorrison]

bors merge

[bors]

Canceled.

[alreadydone]

Since this has been merged into #15663 which is in queue, let me take the opportunity of this PR to speedup to other declarations.

[kbuzzard]

You could leave a comment saying that tidy can do these but you're doing them anyway, but it's probably better to get this merged ASAP

[alreadydone]

You could leave a comment saying that tidy can do these but you're doing them anyway, but it's probably better to get this merged ASAP

I think in general it's reasonable to prefer longer, less-automatic but much faster code over shorter but slower code, and does not need a special explanation. And it's clearly not rare to fill in the map_id'/comp' fields manually as can be seen from the search results.

By the way, I just found out you actually beat me in opening PR (#16872) and had exactly the same changes!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests