Pi instance names in Lean 4 core

Stream: lean4

[Bhavik Mehta]

The instances docs3#pi.inhabited and docs3#pi.subsingleton are auto-named in Lean 4 core, and called docs#instInhabitedForAll_1 and docs#instSubsingletonForAll instead - a few porting notes also comment on this. Would it be sensible to try to rename these? I'd be happy with a mathlib alias or a change in core, since we do have docs#Pi.Fintype and docs#Pi.Nonempty

[Scott Morrison]

@Bhavik Mehta, could you add them as aliases in mathlib, with a link to lean4#2343?

[Eric Wieser]

Is there any reason not to rename these in core, besides being a waste of reviewer time? At this point I've probably spent more time trying to figure out if alias is safe for instances...

[Scott Morrison]

Sorry about this. Just the usual answer: reviewing external PRs at Lean4 is still occupying more time that we have available for it, so wherever possible if fixes can be done downstream we'd prefer that.

Renaming instances by hand is time that could be spent on lean4#2343 instead. :-)