docs: Library note on performance when defining instances

[ChrisHughes24]

---

This method can improve speed, for example #7434, #7435, #7401, #6874, #7408, #7430, #7435, #7436 Sometimes it slows things dow though, e.g #7431

[ChrisHughes24]

Sometimes it is better to avoid with, right? Maybe we can explain more here.

I'm writing instructions with this PR in mind. So after that PR it won't necessarily be best to avoid with. However I should maybe include information about how Lean automatically fills in fields that can be found by type class inference and prioritises whatever is given by with. I don't know how much detail to go into about how extends works and how something like CommGroup extends both Group and CommMonoid, but only has a toGroup field and not a toCommMonoid field. I also don't want it to sound like thinking about this is some requirement, I think it's best if most contributors don't have to know this stuff.

[mattrobball]

My understanding of unification is still mainly anecdotal but this lines up with my expectations.

It might be useful to open this up to a broader discussion on Zulip where we can get some input from core and others.

One point I do know and that is implicit here but might benefit from being made explicit: aligning the inheritance structure for instance construction only matters mainly for data carrying fields.

[mattrobball]

Lean also seems to really dislike unifying instances constructed using differing patterns. My guess that it has to unfold everything on both sides to reach a common state.

[mattrobball]

I solicited some expert opinion on Zulip for any potential refinements.

[fpvandoorn]

I haven't followed this discussion closely, but a library note like this is good (and we can refine it later with more experience). I presume that this library note is still relevant after lean4#2644?

bors d+

[bors[bot]]

:v: ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ChrisHughes24]

I don't think it is still relevant. Or at least the gains are much less. See #7554 . I haven't had time to investigate more closely, but I will probably close my open PRs.

[mattrobball]

Some things are still relevant but it's less clear after leanprover/lean4#2644. My guess is that the jumping up the hierarchy by explicitly a data carrying instance at the top might be counterproductive since the improved defeq cache does a much more efficient job of discharging the checks in between and the fact we are forcing unfolded terms is hurting more.

[fpvandoorn]

Ok, then feel free to close it.

[grunweg]

Coming here from issue triage: what's the current state of this PR?

[ChrisHughes24]

The issue about def-eq performance is no longer relevant after the lean3 PR. There were commits made to improve def-eq performance that referenced this note that are probably no longer important and could be reversed.There are still a bunch of TODOs in mathlib referencing this PR. The changes they are next to are probably no longer important and could be reversed.