mathlib4 porting PRs

Stream: PR reviews

[Scott Morrison]

There's #17039 which adds out first SYNCHRONIZED labels to mathlib, and then also #17056 which updates the port_status.py script to be more flexible handling comments and status information in the port status wiki page. If either/both could have a merge soon that would be nice. :-)

[Johan Commelin]

Thanks, I kicked both of them on the bors queue.

[Scott Morrison]

#17079 is now our first instance of a PR to mathlib that touches a synchronized file, so has an associated mathlib4 PR.

(This is a problem that I noticed while porting.)