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
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.