multilinear timeouts

Stream: general

[Rob Lewis]

I just opened #6639, which speeds up a proof that's causing timeouts in CI. But I'm not sure if the slowness here is related to recent changes or if it's always been there. Any ideas?

[Gabriel Ebner]

I've run into the same issue in a different PR: https://github.com/leanprover-community/mathlib/pull/6045/files#diff-030c8b121453cb0be59dad5f7db3fe154f7bd17ad5ec67167535b9cb68400559

[Gabriel Ebner]

I think the definition is just on the edge of the timeout, and any change is liable to push it over.

[Rob Lewis]

Looking at @Jannis Limperg 's benchmark tool output, this commit added 20 seconds (25%) to normed_space/multilinear.lean

[Rob Lewis]

Which isn't proportional to the lines added, but the file was still slow before

[Sebastien Gouezel]

Looks like https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223001979 is also having an effect, so I disabled some subsingleton instances in this file for further speedup.