During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

… (#17866)

Discussed with @kim-em.

These instances are now necessary because instance synthesis now searches with the full discrimination tree, so mismatches in the arguments to instances are scrutinized much harder. This is not likely to be reverted in the future, so the instances remain required.

There were a few further occurrences of #10670 for Grp, see e.g. [Grp.instCoeFunHomForallαGroup](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/Grp/Basic.html#Grp.instCoeFunHomForall%CE%B1Group). These do look like they are unnecessary but removing them breaks a lot of downstream proofs. (I think it's something to do with `coe_of` unfolding `of` causing a mismatch between the expected types, but it's a bit too subtle to deal with easily.) I'll leave those porting notes for the meantime.

We need a big refactor cleaning up the concrete category bits of the library anyway.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This is the first half of the changes, to see if those work without slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This is the first half of the changes, to see if those work without slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This is the first half of the changes, to see if those work without slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This is the second half of #17870, and doesn't affect the benchmarks.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

I am currently bisecting to figure out exactly why the benchmarks are indicating a slowdown with no obvious cause.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This is the first half of the changes, to see if those work without slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

This contains everything except the interval [1/4, 3/8] of the changes, and doesn't affect the benchmark.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

There is also a shortcut instance that we need for speed reasons: `SemilinearIsometry.instCoeFun`. I don't know why this is so performance-sensitive but the benchmarks tell us that it is.

See also #17871 for removing porting notes and comments where this change happened earlier on.