chore(data/equiv): make `equiv.ext` args use { } (#2776)
Other changes:
* rename lemmas `eq_of_to_fun_eq` to `coe_fn_injective`;
* add `left_inverse.eq_right_inverse` and use it to prove `equiv.ext`.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
