aligns for refactored content

Stream: mathlib4

[Eric Rodriguez]

For mathlib4-only refactors, what should we do with aligns to what stuff was in the past?

[Eric Rodriguez]

what if the content changes a bit of a lemma but not a lot?

[Yury G. Kudryashov]

IMHO, if #align will help someone who ports a project based on mathlib, then it should stay (possibly, with the \_x suffix).

[Scott Morrison]

Let's not use the ₓ suffix, it is not particularly helpful as a warning (everyone already knows that not everything matches up cleanly, and just having an ₓ doesn't give much extra information), and ends up being just noise.

Writing comments, however, is great. :-)

But I certainly agree we should keep the #align's, even as they become approximate hints. I still use grep for #align.*XYZ sometimes.

[Eric Rodriguez]

It's actually kind of nice to be able to search for fully qualified names. I wonder if we could do this for all theorems somehow

[Dagur Asgeirsson]

If I change the name of X to Y, and give the name X to something else, should I

1. move the #align x X to the new X,
2. put #align x Y below Y,
3. both of the above, or
4. remove the #aligns altogether?

[Winston Yin (尹維晨)]

Aligns are to help Mathport find the mathlib4 counterpart to a mathlib3 theorem/definition, so 2. The new X, despite the name, would be a totally new feature in mathlib4 that has no counterpart in mathlib3 to be aligned to.