chore(topology/algebra/module): review `coe` lemmas (#6206)
* add `@[simp]` to `continuous_linear_equiv.coe_coe`, remove from `continuous_linear_equiv.coe_apply`;
* golf `continuous_linear_equiv.ext`;
* given `(e e' : M ≃L[R] M₂)`, simplify `(e : M →L[R] M₂) = e'` to `e = e'`;
* add `@[simp]` to `continuous_linear_equiv.symm_comp_self` and `continuous_linear_equiv.self_comp_symm`;
* drop `symm_comp_self'` and `self_comp_symm'`: now `coe_coe` simplifies LHS to `symm_comp_self`/`self_comp_symm`;
* `continuous_linear_equiv.coord` is no longer an `abbreviation`: without this change `coe_coe` prevents us from using lemmas about `coord`;
