refactor(data/equiv/basic): remove `equiv.set.range` (#6960)
We already had `equiv.of_injective`, which duplicated the API. `of_injective` is the preferred naming, so we change all occurrences accordingly.
This also renames `equiv.set.range_of_left_inverse` to `equiv.of_left_inverse`, to match names like `linear_equiv.of_left_inverse`.
Note that the `congr` and `powerset` definitions which appear in the diff have just been reordered, and are otherwise unchanged.
