porting "unneeded" files

Stream: mathlib4

[Johan Commelin]

The top of "Unported files" on #port-dashboard is slowly being dominated by files that have comments like "not needed" or "essentially already ported to Std4". Probably the best thing to do with these files is to create the corresponding file in mathlib4 and fill it with

• #noalign statements for "not needed"
• #align statements for stuff that has been ported to Std4

[Scott Morrison]

Can we alternatively just remove them from the dashboard (not for two weeks, presumably), or just ignore them?

[Johan Commelin]

I guess the #align statements could potentially be useful...

[Johan Commelin]

Also, I don't know how to hack on the backend of #port-dashboard

[Johan Commelin]

I think I'll just create a bunch of PRs for these files when I'm at my office pc.