chore(*): add a few more `unique` instances (#4511)
* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
`continuous_linear_map.unique_of_left`,
`continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
`subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
`unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
`function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`;
* rename `linear_map.coe_inj` to `coe_injective` and `continuous_linear_map.coe_inj` to `coe_fn_injective`,
make them use `function.injective`.
Motivated by #4407
