feat(ci): switch from mergify to bors (#2322)
This PR (joint work with @gebner) changes the automation that merges our PRs from mergify to a service called [bors](https://bors.tech/). Currently, the "time-to-master" of an approved PR grows linearly with the number of currently queued PRs, since mergify builds PRs against master one at a time. bors batches approved PRs together before building them against master so that most PRs should merge within 2*(current build time).
As far as day-to-day use goes, the main difference is that maintainers will approve PRs by commenting with the magic words "`bors r+`" instead of "approving" on Github and adding the "ready-to-merge" label. Contributors should be aware that pushing additional commits to an approved PR will now require a new approval.
Some longer notes on bors and mathlib can be found [here](https://github.com/leanprover-community/mathlib/blob/2ea15d65c32574aaf513e27feb24424354340eea/docs/contribute/bors.md).
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
