mathlib4#549

Stream: mathlib4

[Jireh Loreaux]

I have now had a thorough look at this PR, but I have made a bunch of changes there, so someone else should now review.

[Scott Morrison]

Thanks @Ruben Van de Velde. Just a general note to everyone; it's helpful if when you give reviews of PRs you adjust the tags accordingly (e.g. in this case switching it back to awaiting-author). This is helpful for notifying authors, and allowing other reviewers/maintainers to focus on the active tasks.

[Yakov Pechersky]

:ping_pong: