[Merged by Bors] - chore: adaptations to lean 4.8.0

[Ruben-VandeVelde]

Mainly this adds names to instances, which are presumably necessary for some unspecified reason.

---

[eric-wieser]

Can you add an explanation of why all the instances were renamed?

The new names are fine, but I thought the new lean release was supposed to be better at naming them automatically; and it's strange to only give a name to one instance in a group of multiple.

(No changes needed to the diff, just a quick summary in the PR description is enough)

[eric-wieser]

bors d+

[mathlib-bors]

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

bors merge

[semorrison]

bors p=5

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

[kmill]

@eric-wieser I see a reason didn't make it in, but I'll record it here: there are a number of instances that are referred to in the docs, like the overview and the undergrad yaml files. The instance name changes (at least the ones I did) are giving the new names according to the new algorithm.

[Ruben-VandeVelde]

What Kyle said - and it's more robust to give explicit names when we're going to refer to them by name

[eric-wieser]

Thanks! I was curious to know if the issue was name collisions in the new algorithm. I guess the answer is no?