Slowness of `affine_combination`

Stream: general

[Joseph Myers]

Lean seems to be very slow at elaborating calls to docs#finset.affine_combination.

In #17912 I have a lemma whose statement involves six calls to affine_combination, where it's necessary to express three of them in the form @finset.affine_combination R V _ _ _ _ _ _ s p w instead of the desired s.affine_combination p w to avoid elaboration of the lemma statement timing out (this is about the statement, not the proof, and the slowness applies even if the proof is sorry) - I don't think it matters which three are expressed in that form, though I didn't try lots of variants. The issue isn't at all specific to that PR, however - the slowness can be seem for lots of lemma statements in linear_algebra.affine_space.combination, it's just that six uses of affine_combination in the same lemma statement is enough for the slowness to result in a timeout.

Can someone figure out why Lean is so slow working with affine_combination and how to fix that slowness?