chore(*): regularize naming using injective (#3071)
This begins some of the naming regularization discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.20of.20injectivity.20lemmas
Some general rules:
1. Lemmas should have `injective` in the name iff they have `injective` in the conclusion
2. `X_injective` is preferable to `injective_X`.
3. Unidirectional `inj` lemmas should be dropped in favour of bidirectional ones.
Mostly, this PR tried to fix the names of lemmas that conclude `injective` (also `surjective` and `bijective`, but they seemed to be much better already).
A lot of the changes are from `injective_X` to `X_injective` style
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
