Timeout tips?

Stream: new members

[Bjørn Kjos-Hanssen]

I have a 445 line file that suffers from (deterministic) timeout problems. Are there some easy ways to avoid that?
Is the use of tactics likely to compound the problem?
Maybe I should be separating some parts into other files and use import?

[Scott Morrison]

It's typically single declarations that are the problem. Splitting into multiple files won't help.

[Scott Morrison]

Instead break out smaller lemmas.

[Scott Morrison]

It is usually, but not always, tactics that cause timeouts. However unification ("heavy rfl") can be arbitrarily slow! Often this can be fixed by making definitions (more) irreducible.

[Bjørn Kjos-Hanssen]

Thanks @Scott Morrison

[Kevin Buzzard]

Feel free to post working code if you want people to make more precise comments. Note that it has to run though (all imports, definitions etc must be there).