fix: make sure AbstracNestedProofs.visit doesn't fail due to transparency issues

[arthur-adjedj]

This PR ensures the isNonTrivialProof call in AbstracNestedProofs.visit runs with enough transparency to not trigger errors during its potential inferType call. This is needed when abstracting over proofs that may be needed to reduce a structurally recursive function eliminating from Prop to Type.

In preparation for #12718.

[arthur-adjedj]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@3898df9 against leanprover-community/mathlib4-nightly-testing@d448452 are in! @arthur-adjedj

• build//instructions: -24.8G (-0.01%)

No significant changes detected.

[arthur-adjedj]

changelog-language

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-28 18:47:49)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12740 has successfully built against this PR. (2026-02-28 19:42:29) View Log

[nomeata]

The test suite is currently revamped by @Garmelon, that could be related.

[nomeata]

Thanks for this fix. As discussed privately, this change is possibly, maybe even likely, benign, but touches a core component with a big blast radius, and reducibility issues are always hairy, so I cannot vouch for this change and the existing motivation (issue #12739) is not quite strong enough to take the risks or to spend more time thinking about it.