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