Commit 2024-06-26 05:43 d803ff3b

feat: if the body constrains universes, make it explicit in the signature. (#14069) In many places in Mathlib universes in the type signature are invisibly constrained by the RHS of the def. This PR makes all these explicit in the type signature. Likely we will change the Lean behaviour to disallow this in https://github.com/leanprover/lean4/pull/4482 (i.e. this is the backport to master of the fixes required for that).