# Are there squeeze-versions of ring and abel?

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.

• No, there isn't. You could try show_term { ... } and replace it with that, though. Jan 12 at 11:22

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!