perf: optimize Key.hash at DiscrTree for the .const constructor

[JovanGerb]

This PR optimized Key.hash at for DiscrTree in the Key.const case. This is the most common case, and is computed regularly during type class search and simp.

[nomeata]

Do you have performance data that shows that this is relevant and worth the effort of a PR? (The reduced uniformity of the cases make me uneasy. Will this introduce new collisions with other constructors?)

[JovanGerb]

Not yet, I'll bench it on mathlib when it builds

[JovanGerb]

I don't really see how this could lead to more collisions. If you think it is better, I could move the mixHash 5237 $ over to the .proj constructor, since that one apparenly also doesn't have any explicit number in its hash function

[nomeata]

I'm not claiming to be an expert of this crucial code; if the performance gains are meausurable and significant then it shounds like it's worth for me to become one to be able to review it properly.

[nomeata]

(btw, if you want to run experiments before drawing attention from reviewers, then leaving the PR in draft mode signals that)

[JovanGerb]

@nomeata, I guess we won't find out as there seems to be something weird going wrong with the build.