refactor(*): Add `_injective` alongside `_inj` lemmas (#5150)
This adds four new `injective` lemmas:
* `list.append_right_injective`
* `list.append_left_injective`
* `sub_right_injective`
* `sub_left_injective`
It also replaces as many `*_inj` lemmas as possible with an implementation of `*_injective.eq_iff`, to make it clear that the lemmas are just aliases of each other.
