mathlib3

15712902 - feat(logic/is_empty): add some simp lemmas and unique instances (#7832)

feat(logic/is_empty): add some simp lemmas and unique instances (#7832) There are a handful of lemmas about `(h : ¬nonempty a)` that if restated in terms of `[is_empty a]` become suitable for `simp` or as `instance`s. This adjusts some of those lemmas.