fix: build casesOn for propositions from projections

[nomeata]

This PR makes casesOn and recOn of a proposition apply the minor premise to the projections of the major premise, instead of going through the recursor. A recursor only reduces once its major premise is a constructor application, which a proof may never become, so And.casesOn and friends no longer require the proof itself to reduce.

This matters for proofs that abstractNestedProofs has moved into auxiliary theorems, whose values are not available for reduction: the module system does not expose them outside their defining module, and theorems are opaque. An abstracted proof of an And that is stored in a Subtype and later pattern-matched, or eliminated into data directly, otherwise makes the enclosing definition ill-typed.

Lean.mkCasesOnViaProjs? applies to a proposition with a single constructor, no indices and no recursion, whose recursor supports large elimination. Large elimination forces every field to be a proof, which is what makes the projections available, since projecting data out of a proposition is what Exists may not do. The minor premise expects the fields of I.mk x₁ … xₙ rather than those of the major premise, but both are proofs of the same proposition, so proof irrelevance identifies them.

tests/elab_fail/etaStructIssue.lean moves to tests/elab: both of its sides now reduce to mkNat e applied to a proof of F e, which proof irrelevance identifies, and the elaborator and the kernel agree on that.

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 8f5e057 against 47680c2 are in. There are significant results. @nomeata

• ✅ build//instructions: -1.4G (-0.01%)

Large changes (1✅, 2🟥)

• ✅ compiled/rbmap_checkpoint//instructions: -735.1M (-5.47%)
• 🟥 elab/bv_stress_structures_1//instructions: +3.4G (+23.09%)
• 🟥 elab/bv_stress_structures_2//instructions: +3.5G (+19.83%)

Medium changes (1🟥)

• 🟥 compiled/rbmap_checkpoint//maxrss: +2MiB (+0.08%)

Small changes (3✅, 4🟥)

• 🟥 build/module/Lean.Meta.Constructions.CasesOn//instructions: +622.7M (+46.42%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Constructions.RecOn//instructions: +39.6M (+3.22%)
• ✅ compiled/rbmap_checkpoint//task-clock: -101ms (-6.33%)
• ✅ compiled/rbmap_checkpoint//wall-clock: -103ms (-6.42%)
• 🟥 elab/bv_stress_structures_1//wall-clock: +258ms (+24.21%)
• 🟥 elab/bv_stress_structures_2//wall-clock: +254ms (+20.95%)
• ✅ elab/whnfMatcherImplicitTransparencyCaching//instructions: -69.0M (-0.28%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47680c2e62831da4daa01abe567b3e4fc509fbae --onto fd0efc4306a7773c2cd4e079ddaa907426d0f5da. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 10:16:43)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0dc10a41e6be57ef72d7f103c98c263620076b6c --onto fd0efc4306a7773c2cd4e079ddaa907426d0f5da. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 11:44:59)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 47680c2e62831da4daa01abe567b3e4fc509fbae --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-25 10:16:45)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0dc10a41e6be57ef72d7f103c98c263620076b6c --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-25 11:45:01)