mathlib3

10c57eb0 - Fix the remaining things and restore Bhavik's proof