mathlib3

24a793aa - trying to automate that compactness is hygienic