feat: drop the universe bump from PSigma, PProd and PULift

[nomeata]

This PR gives PSigma, PProd and PULift the resulting universe Sort (max u v) instead of Sort (max 1 u v), so a pair of propositions is itself a proposition and lifting a proposition yields a proposition. Their recursors are correspondingly restricted to motives in Prop, while casesOn and recOn stay universe-polymorphic. The structure command now accepts such a resulting universe, subject to bootstrap.inductiveCheckResultingUniverse as inductive already was.

The kernel restricts the recursor of a single-constructor type whose resulting universe can be Prop. Projections stay available, since the field-universe check forces every field of such a type to be a proof whenever the type is one, so Lean.mkCasesOnViaProjs? builds casesOn and recOn from Expr.proj plus eta for structures. Everything derived from casesOn is unaffected; SizeOf used the recursor directly and gets a projection-based path of its own, and the guards that read "can eliminate into Type" off .rec's level parameters now read it off .casesOn.

The bump no longer leaks into the universe levels of below. Lean.Meta.PProdN still packs propositions with And rather than PProd, but that is now only for readability rather than to stay in Prop.

A tuple of proofs is now a proof, so it gets abstracted into an auxiliary theorem and a packed well-founded recursion argument is no longer a manifest chain of PSigma.mk. ArgsPacker.Unary.unpack therefore falls back to projections, which are always valid here, and FunInd.cleanPackedArgs reduces PSigma.casesOn applied to a proof. MatcherApp.transform gained addProofEqualities so that functional induction keeps substituting a proof-valued discriminant away instead of leaving a dead binder in the principle; only homogeneous equations are added, since a heterogeneous one cannot be substituted. casesOnStuckLHS now reduces the major premise before looking for the variable to case on, and runs in the goal's local context.

T.ctorElimType loses its bump as well: the lookup table holding the constructor-elimination types is declared in the universe of its entries, which is no longer raised past Prop by PULift, so eliminating into a proposition no longer lifts those types into Type.

Subtype would be eligible for the same treatment — its fields are a value and a proof about that value, so a subtype of a proposition is a proposition — but it is left alone here, because building casesOn from projections has a bad effect on meta code. Such a casesOn reduces on any scrutinee rather than getting stuck on a variable, so a match on the type is no longer a case split: the proof in ⟨x, _⟩ stops being determined by unification whenever the callee matches on the subtype (22 such sites in Std.Data.DHashMap.Lemmas alone), well-founded recursion loses the split it needs to find a decreasing measure (tests/elab/grind_qsort.lean), and match equation generation fails (tests/elab/adamTC.lean). The types touched here are internal enough that this does not come up for them, but Subtype is written by hand all the time. None of it would arise if the kernel gave such a type a large-eliminating recursor, which would be reasonable: whenever the type is a proposition every one of its fields is a proof, so it is a subsingleton and no impredicativity is being exploited, exactly as for And, whose recursor already eliminates into any universe.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_014KdqrCEybAM2f7AKbAsJsx

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 978cfd5 against e9c0364 are in. There are significant results. @nomeata

• ✅ build//instructions: -11.1G (-0.10%)

Medium changes (2✅, 1🟥)

• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -1.7G (-3.20%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -4.3G (-5.05%) (reduced significance based on absolute threshold)
• 🟥 compiled/rbmap_checkpoint//instructions: +23.0M (+0.18%)

Small changes (51✅, 9🟥)

• ✅ build/module/Init.Data.Array.Basic//instructions: -31.2M (-0.29%)
• ✅ build/module/Init.Data.Array.BasicAux//instructions: -19.9M (-1.38%)
• ✅ build/module/Init.Data.Array.BinSearch//instructions: -116.3M (-1.97%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Bootstrap//instructions: -38.4M (-1.66%)
• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +56.7M (+0.56%)
• ✅ build/module/Init.Data.Array.Sort.Basic//instructions: -88.5M (-3.36%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Fin.Iterate//instructions: -16.2M (-1.80%)
• ✅ build/module/Init.Data.Iterators.Consumers.Monadic.Loop//instructions: -18.7M (-0.43%)
• ✅ build/module/Init.Data.List.Sort.Basic//instructions: -17.8M (-0.70%)
• ✅ build/module/Init.Data.List.Sort.Impl//instructions: -87.3M (-0.79%)
• ✅ build/module/Init.Data.Range.Basic//instructions: -28.3M (-0.84%)
• ✅ build/module/Init.Data.Range.Polymorphic.RangeIterator//instructions: -99.7M (-0.52%)
• ✅ build/module/Init.Data.String.Extra//instructions: -51.1M (-1.79%)
• ✅ build/module/Init.Data.String.Legacy//instructions: -90.4M (-4.91%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.String.Lemmas.Pattern.Split.Basic//instructions: -23.7M (-0.77%)
• ✅ build/module/Init.Data.String.Substring//instructions: -45.6M (-1.24%)
• ✅ build/module/Init.Data.Vector.Basic//instructions: -25.0M (-0.33%)
• ✅ build/module/Init.Data.Vector.OfFn//instructions: -20.7M (-0.47%)
• ✅ build/module/Lake.Load.Resolve//instructions: -78.9M (-0.95%)
• ✅ build/module/Lake.Util.Version//instructions: -47.1M (-0.69%)
• and 40 more

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-22 19:55:31)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-21 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-08-22 19:55:32)

[nomeata]

This probably needs #14901 fixed first.

[plp127]

Can we fix Subtype too?

[nomeata]

Subtype would be eligible for the same treatment — its fields are a value and a proof about that value, so a subtype of a proposition is a proposition — but it is left alone here, because building casesOn from projections has a bad effect on meta code. Such a casesOn reduces on any scrutinee rather than getting stuck on a variable, so a match on the type is no longer a case split: the proof in ⟨x, _⟩ stops being determined by unification whenever the callee matches on the subtype (22 such sites in Std.Data.DHashMap.Lemmas alone), well-founded recursion loses the split it needs to find a decreasing measure (tests/elab/grind_qsort.lean), and match equation generation fails (tests/elab/adamTC.lean). The types touched here are internal enough that this does not come up for them, but Subtype is written by hand all the time.