mathlib

14b69e9f - refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542)

refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542) The `inhabited` typeclass is intended to be a default value (and computable, if one is writing programs) but many times it is filled in with a junk (and perhaps noncomputable) value to satisfy the `has_inhabited_instance` linter. This commit switches to a `has_nonempty_instance` linter to push contributors toward supplying a `nonempty` instance instead. The linter still accepts `inhabited` and `unique` instances, which should be preferred over `nonempty` when appropriate.