[Merged by Bors] - feat: if the body constrains universes, make it explicit in the signature.

[kim-em]

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 leanprover/lean4#4482 (i.e. this is the backport to master of the fixes required for that).

[github-actions]

PR summary b30ac189df

Import changes

No significant changes to the import graph

---

Declarations diff

+ instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] (X Y : C) : Small.{w, v} (X ⟶ Y)
+ instance (F : C ⥤ D) [PreservesEffectiveEpiFamilies.{_, _, 0} F] :
+ instance (F : C ⥤ D) [ReflectsEffectiveEpiFamilies.{_, _, 0} F] :
+ instance : EssentiallySmall.{u} LightDiagram.{u}
+ instance : EssentiallySmall.{u} LightProfinite.{u}
+ instance : HasLimitsOfSize.{u, u + 1} (CondensedMod.{u} R)
+ instance : HasLimitsOfSize.{u, u + 1} CondensedSet.{u}
+ instance [(forget D).IsRightAdjoint] : (sheafForget (D := D) J).IsRightAdjoint
+ instance [HasColimits.{v, u} C] (X : TopCat.{w}) : HasColimitsOfSize.{v, v} (Presheaf C X)
+ instance [HasLimits C] (X : TopCat) : CreatesLimits.{v, v} (Sheaf.forget C X)
+ instance [HasLimits C] (X : TopCat.{v}) : HasLimits.{v} (Presheaf C X)
+ instance [HasLimits C] (X : TopCat.{v}) : HasLimitsOfSize.{v, v} (Sheaf.{v} C X)
+ instance [HasLimits C] : HasColimits.{v} (SheafedSpace C)
- instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] (X Y : C) : Small (X ⟶ Y)
- instance (F : C ⥤ D) [PreservesEffectiveEpiFamilies F] : PreservesFiniteEffectiveEpiFamilies F
- instance (F : C ⥤ D) [ReflectsEffectiveEpiFamilies F] : ReflectsFiniteEffectiveEpiFamilies F
- instance : EssentiallySmall LightDiagram.{u}
- instance : EssentiallySmall LightProfinite.{u}
- instance : HasLimitsOfSize.{u} (CondensedMod.{u} R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
- instance : HasLimitsOfSize.{u} CondensedSet.{u} := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
- instance [(forget D).IsRightAdjoint ] : (sheafForget J : Sheaf J D ⥤ _).IsRightAdjoint
- instance [HasColimits C] (X : TopCat) : HasColimitsOfSize.{v} (Presheaf C X)
- instance [HasLimits C] (X : TopCat) : CreatesLimits (Sheaf.forget C X)
- instance [HasLimits C] (X : TopCat) : HasLimits (Presheaf C X)
- instance [HasLimits C] (X : TopCat) : HasLimitsOfSize.{v} (Sheaf.{v} C X)
- instance [HasLimits C] : HasColimits (SheafedSpace C)

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[YaelDillies]

The other changes look good.

Just to make sure, by RHS you mean example : LHS := RHS, not example : LHS = RHS := ...? I would rather call that the "body" of the declaration.

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style