Commit 2026-10-03 02:35 300d0e53

perf: speed up FunLike synthesis (#44317) This PR speeds up synthesis of FunLike and hence of CoeFun. This is important because the elaborator uses this type class to insert coercions. See also the old refactor #8386 which was motivated by the same idea. I've added a test file to avoid future regressions. The instance RKHS.instFunLike used to take a long time to fail because it would search for instances of RCLike ?𝕜, (which has multiple options that all need to be tried!). I've changed the syntesis order of the instance to improve this. If anyone has an idea for how to get rid of this instance altogether that would be great. This PR mostly touches leaf files, so this change doesn't speed up mathlib much. But it will speed up any file that imports all of mathlib.