Are there squeeze-versions of ring and abel?

Question

In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons:

(1) Otherwise the behaviour of simp might change, when for example mathlib is changed.

(2) The proof-verification runs faster, since simp does not have to try all lemmas.

I am wondering whether there are similar commands for other tacticts, such as ring or abel. If I understand correctly, the behaviour (point (1)) is fixed, but for point (2) this could lead to an improvement.

Concretely, I have a long proof that uses a bunch of abel and it returns a deterministic timeout, so I would like to speed it up.

Answer 1

Both ring and abel produce a proof term that is going to be about as good as you could hope for from a putative squeeze_ring or squeeze_abel. This explains the suggestion from the comment to use show_term { ring }. However you will quickly find that for all but the most trivial examples, this will produce very large proof terms that you will not want to copy and paste into your source file!

The general answer to "I have a long proof and ..." is to split your proof into many smaller lemmas. (I aim for at most 10 lines, and if the proof "has to" be longer, to make sure there are human-readable expository comments at least every ten lines.) Smaller lemmas are usually easier for humans to digest, and more maintainable, as well as often faster to elaborate (and less likely to hit the deterministic timeout limit).