RFC: Standardise naming for instances

Currently, we have 300+ instances with a manual name like instance instCommGroup : CommGroup _, and 700+ instances with a manual name that does not contain inst.

I think not having a standardised policy for these names can create confusion, so I urge the community to decide on one standard for the future.

Arguments for inst:

• Kenny (the author) thinks that this is more consistent with the automatically generated names, which reduces the burden on the user when trying to guess the name, as it is inefficient to first try Rat.commRing and then Rat.instCommRing.

Arguments against inst:

• Andrew Yang thinks that the automatically generated names are intentionally different to discourage people from mentioning them.

There also seem to be people with the opinion that we should not have explicit instance names at all, which is also one possible option.

Zulip: mathlib4 > naming convention: "inst" in instance names

Start by reviewing the linked instance-name search results and the Zulip discussion on the naming convention. The work is done when the community reaches a documented decision on a standard for explicit instance names and the issue records that decision.