mathlib3

8983bec7 - fix(data/set_like): `coe_sort_trans` should have low priority (#15489)

fix(data/set_like): `coe_sort_trans` should have low priority (#15489) In core Lean, `coe_sort_trans` is given default priority, meaning it takes precedence over `set_like.has_coe_to_sort`. As a consequence, sometimes a weird instance path was chosen, such as `submodule R M → Module R → Type*` rather than the direct path `submodule R M → Type*`, and I believe this can lead to diamonds (including weird universe levels), and in any case to weird defeq checks (which are made extra expensive by occurring in the type). In fact, there are quite a few `has_coe_to_sort` instances that would be useless since they are preceded by a `has_coe`, e.g. `lie_ideal`. Lowering the priority of `coe_sort_trans` below that of `set_like.has_coe_to_sort` should ensure we use the preferred inheritance path. We did the same thing for `coe_fn_trans` in `fun_like/basic.lean`. The consequence is that certain places that (ab)used the weird coercion paths will need to be slightly redefined to use the new path, basically inserting unification hints manually. Those paths were slightly fragile anyway so I don't think that's an important loss compared to the advantages of clarifying.