mathlib3

0d140b15 - feat(data/set/basic): nonempty instances for subtypes (#5409)

feat(data/set/basic): nonempty instances for subtypes (#5409) In #5408, it is useful to be able to track the nonemptiness of a subset by typeclass inference. These constructions allow one to do this.