mathlib

38a5388c - wip(data/subtype_instances): introduce closed_under predicate typeclasses