mathlib 3 ready to merge PR

Stream: mathlib4

[Kevin Buzzard]

RE step 8 of the porting procedure on the wiki: I have already made the mathlib3 "freeze" PR https://github.com/leanprover-community/mathlib/pull/17324 for a mathlib4 port PR https://github.com/leanprover-community/mathlib4/pull/534 because I felt it was "part of the job". Is the idea that I wait until the mathlib4 PR to be merged before I mark the mathlib3 PR as ready for review? Or have I already made an error by making the PR early?

[Scott Morrison]

I think we're still working this out. I think it may be best if we don't treat this as part of the job for each separate file, but rather something we can do in bulk, as in #17314.

Recall that scripts/port_status.py now has a section in the output that list all files that are marked as Yes in #port-status, but that don't have synchronization warnings in mathlib. Thus it's easy to do a single sweep to catch up.

[Scott Morrison]

(and in fact as of #17314, scripts/port_status.py includes the PR number in its output.)