Remaining proposed syl renames (group 2)

[jkingdon]

These had their roots in a proposal by Norm which has received some refinement, discussion, and action since.

The proposed changes are listed in changes-set.txt and the division into groups is from #4332 (comment) . Group 1 from that comment is done, this issue is about group 2, and #4505 is for groups 3 and 4.

The proposed renames in group 2 are:

proposed syld imtrd
proposed sylbi biimtri
proposed sylib imbitri
proposed sylibr imbitrri
proposed sylbir biimtrri
proposed sylibd imbitrd
proposed sylbid biimtrd
proposed sylibrd imbitrrd
proposed sylbird biimtrrd
proposed syl5bi biimtrid done
proposed syl5bir biimtrrid
proposed syl5ib imbitrid
proposed syl5ibr imbitrrid
proposed syl6ib imbitrdi
proposed syl6ibr imbitrrdi
proposed syl6bi biimtrdi
proposed syl6bir biimtrrdi

and I grouped them this way because the new names seem fairly obvious to me based on the patterns we have established in the past.

Feel free to make suggestions for alternate names or any of these that aren't a good idea, but unless we hear otherwise, I think we can all assume these are a good idea and we're ready to start making pull requests.

Some guidelines based on our recent experience:

• If doing a rename in multiple pull requests, put in a comment on the old name saying it is being renamed, but don't use New usage is discouraged (that just makes merge conflicts in the discouraged file more likely, and doesn't seem to have significant benefits for this purpose).
• We tend to merge rename pull requests quickly to reduce the potential for merge conflicts.

[tirix]

My remark would be that most, if not all of these renames increase the length of the theorem name. For example from sylib to imbitri there are 2 more characters in the name. With more than 3000 occurrences of sylib, that's at least 6kb more for set.mm, while others (not me!) are making efforts to shorten the database by sometimes a few bytes.

But clearly here we want to be more expressing, and there is no way to carry more information in the name while being as short as a numbering, so this is probably the lesser of two evils.

[benjub]

that's at least 6kb more for set.mm, while others (not me!) are making efforts to shorten the database by sometimes a few bytes.

It is misleading to put these two things in comparison: the shortenings seek to reduce the number of proof steps: that translates into byte reduction, but that is only a byproduct, not the objective.