Generalising #align-ed declarations

Stream: mathlib4

[Michael Rothgang]

This question came up during review: what's the policy for #align-ed declarations which are generalised in a PR? Should one

• remove the #align? I presume not (yet)
• change the align to the new lemma, which is more general?
• keep the old lemma, as a special case of the new one?

I guess this may depend on the particular case: if the special case is worth having anyway, e.g. because it's the most commonly used variant, the last option is clearly the one to go. But suppose the general version is actually preferrable... what do you think?

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/aligns.20for.20refactored.20content/near/377427884 seems related, but not quite the same.

[Mario Carneiro]

if it's a drop in replacement, it's usually best to make the #align target the new lemma

[Mario Carneiro]

You should never remove #align's, that's usually the worst option because it means mathport won't have any idea what to align to and will make some nonsense. Even if the type has changed such that it won't compile anymore as is it's still better than nothing to point to the revised lemma because that's one less thing to manually look up the name of during the fixup phase