mathlib

ff996689 - feat(data/*): `unique` instances for `dfinsupp` and `direct_sum` (#16017)

feat(data/*): `unique` instances for `dfinsupp` and `direct_sum` (#16017) + Add `unique` instances when the codomain types are subsingletons and rename the original `unique` instances (which apply when the domain is empty) to `unique_of_is_empty`. These are in analogy to [pi.unique](https://leanprover-community.github.io/mathlib_docs/logic/unique.html#pi.unique) and [pi.unique_of_is_empty](https://leanprover-community.github.io/mathlib_docs/logic/unique.html#pi.unique_of_is_empty). + Golf the `unique` instances for (d)finsupp using `fun_like.coe_injective.unique`. The names `unique_of_left` and `unique_of_right` remain unchanged in the finsupp case, because finsupp is special in that it consists of non-dependent functions, unlike dfinsupp or direct_sum. (There was a concern that adding `unique` instances would slow down `simp` (see #6025), but it has been fixed in [lean#665](https://github.com/leanprover-community/lean/pull/665).)