Strange timeout

Stream: general

[Heather Macbeth]

I'd be glad of help diagnosing a timeout at the lemma has_sum_repr_symm in #11255. I discussed with @Rob Lewis and he also couldn't see the issue.

I don't really have ideas for speeding it up -- I already rewrote to avoid all simps, for example. I actually get "goals accomplished" in VSCode for this proof, but the timeout shows up just the same.

[Rob Lewis]

The proof is complete, but the kernel hates it. I get the same timeout trying to add the declaration with a metaprogram.

[Heather Macbeth]

#11255 is now ready for review, I'd like to bump this question about a strange timeout in it!