fix: abstractNestedProofs should see into the head of an application

[JovanGerb]

This PR changes abstractNestedProofs so that it also visits the subterms in the head of an application.

This oversight caused some definitions in mathlib to have unabstracted proofs, such as CategoryTheory.StructuredArrow.commaMapEquivalenceInverse

Mathlib bench:
build instructions -0,141 %
process pre-definitions 5,541 %

There is a small general slowdown from the extra work done by abstractNestedProofs . But this is outweighed by the speedup that we get in files related to CategoryTheory.Functor.

Zulip: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/dsimp.20simplifies.20proofs.2C.20which.20is.20slow/near/503630173

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-7353 has successfully built against this PR. (2025-03-05 23:49:54) View Log
• ✅ Mathlib branch lean-pr-testing-7353 has successfully built against this PR. (2025-03-06 00:53:45) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ca0d8226192e7c0cdcc71d6322c3226ad4f73f30 --onto 5536281238dff2fb4e0a54da472d4f0d6496069e. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-06 08:40:09)

[nomeata]

Looks good, thanks! Especially as I'm also experimenting with abstracting more proofs at the moment.

[nomeata]

Can you fix the tests (again)?

[JovanGerb]

Hmm, this test is really annoying because it keeps changing the order of its messages (hence the merge conflict)

[nomeata]

Actually, given that this is a performance critical function, could you maybe make another measurement with the old code that looks at a full application as a whole (but of course fixed to also visit the function). Partial applications are never proofs, and it may make a difference to not look up the cache for every partial application in the term. (Or maybe the proposed code is better if partial applications are shared - who knows)