mathlib3

8877606b - chore(ci): teach bors and GitHub about new labels (#4146)

chore(ci): teach bors and GitHub about new labels (#4146) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>