add missing #align statements !4#1902

Stream: mathlib4

[Johan Commelin]

This PR is the result of a slight variant on the following "algorithm"

• take all mathlib 3 names, remove _ and make all uppercase letters into lowercase
• take all mathlib 4 names, remove _ and make all uppercase letters into lowercase
• look for matches, and create pairs (original_lean3_name, OriginalLean4Name)
• for pairs that do not have an align statement:
  • use Lean 4 to lookup the file + position of the Lean 4 name
  • add an #align statement just before the next empty line
• manually fix some tiny mistakes (e.g., empty lines in proofs might cause the #align statement to have been inserted too early)

[Johan Commelin]

(j/w with Reid)

[Kevin Buzzard]

Very nice idea!

[Kevin Buzzard]

I just spent a rather weird hour reviewing this ;-)