feat: if the body constrains universes, make it explicit in the signa…

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

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -50,7 +50,7 @@ open CategoryTheory Limits
 
 namespace ModuleCat
 
-universe v u₁ u₂ u₃
+universe v u₁ u₂ u₃ w
 
 namespace RestrictScalars
 
@@ -618,11 +618,11 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
 #align category_theory.Module.restrict_coextend_scalars_adj ModuleCat.restrictCoextendScalarsAdj
 
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
-    (restrictScalars f).IsLeftAdjoint  :=
+    (restrictScalars.{max u₂ w} f).IsLeftAdjoint  :=
   (restrictCoextendScalarsAdj f).isLeftAdjoint
 
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
-    (coextendScalars f).IsRightAdjoint  :=
+    (coextendScalars.{u₁, u₂, max u₂ w} f).IsRightAdjoint  :=
   (restrictCoextendScalarsAdj f).isRightAdjoint
 
 namespace ExtendRestrictScalarsAdj
@@ -857,11 +857,11 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR
 #align category_theory.Module.extend_restrict_scalars_adj ModuleCat.extendRestrictScalarsAdj
 
 instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
-    (extendScalars f).IsLeftAdjoint :=
+    (extendScalars.{u₁, u₂, max u₂ w} f).IsLeftAdjoint :=
   (extendRestrictScalarsAdj f).isLeftAdjoint
 
 instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
-    (restrictScalars f).IsRightAdjoint :=
+    (restrictScalars.{max u₂ w, u₁, u₂} f).IsRightAdjoint :=
   (extendRestrictScalarsAdj f).isRightAdjoint
 
 noncomputable instance preservesLimitRestrictScalars

Mathlib/CategoryTheory/Category/Grpd.lean

@@ -135,7 +135,7 @@ def piLimitFanIsLimit ⦃J : Type u⦄ (F : J → Grpd.{u, u}) : Limits.IsLimit
 set_option linter.uppercaseLean3 false in
 #align category_theory.Groupoid.pi_limit_fan_is_limit CategoryTheory.Grpd.piLimitFanIsLimit
 
-instance has_pi : Limits.HasProducts Grpd.{u, u} :=
+instance has_pi : Limits.HasProducts.{u} Grpd.{u, u} :=
   Limits.hasProducts_of_limit_fans (by apply piLimitFan) (by apply piLimitFanIsLimit)
 set_option linter.uppercaseLean3 false in
 #align category_theory.Groupoid.has_pi CategoryTheory.Grpd.has_pi

Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

@@ -103,11 +103,11 @@ class PreservesEffectiveEpiFamilies (F : C ⥤ D) : Prop where
   A functor preserves effective epimorphic families if it maps effective epimorphic families to
   effective epimorphic families.
   -/
-  preserves : ∀ {α : Type*} {B : C} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π],
+  preserves : ∀ {α : Type u} {B : C} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π],
     EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a  ↦ F.map (π a))
 
-instance map_effectiveEpiFamily (F : C ⥤ D) [F.PreservesEffectiveEpiFamilies]
-    {α : Type*} {B : C} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] :
+instance map_effectiveEpiFamily (F : C ⥤ D) [PreservesEffectiveEpiFamilies.{_, _, u} F]
+    {α : Type u} {B : C} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] :
     EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a  ↦ F.map (π a)) :=
   PreservesEffectiveEpiFamilies.preserves X π
 
@@ -128,7 +128,8 @@ instance map_finite_effectiveEpiFamily (F : C ⥤ D) [F.PreservesFiniteEffective
     EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a  ↦ F.map (π a)) :=
   PreservesFiniteEffectiveEpiFamilies.preserves X π
 
-instance (F : C ⥤ D) [PreservesEffectiveEpiFamilies F] : PreservesFiniteEffectiveEpiFamilies F where
+instance (F : C ⥤ D) [PreservesEffectiveEpiFamilies.{_, _, 0} F] :
+    PreservesFiniteEffectiveEpiFamilies F where
   preserves _ _ := inferInstance
 
 instance (F : C ⥤ D) [PreservesFiniteEffectiveEpiFamilies F] : PreservesEffectiveEpis F where
@@ -191,7 +192,8 @@ lemma finite_effectiveEpiFamily_of_map (F : C ⥤ D) [ReflectsFiniteEffectiveEpi
     EffectiveEpiFamily X π :=
   ReflectsFiniteEffectiveEpiFamilies.reflects X π h
 
-instance (F : C ⥤ D) [ReflectsEffectiveEpiFamilies F] : ReflectsFiniteEffectiveEpiFamilies F where
+instance (F : C ⥤ D) [ReflectsEffectiveEpiFamilies.{_, _, 0} F] :
+    ReflectsFiniteEffectiveEpiFamilies F where
   reflects _ _ h := by
     have := F.effectiveEpiFamily_of_map _ _ h
     infer_instance

Mathlib/CategoryTheory/EssentiallySmall.lean

@@ -96,7 +96,7 @@ class LocallySmall (C : Type u) [Category.{v} C] : Prop where
   hom_small : ∀ X Y : C, Small.{w} (X ⟶ Y) := by infer_instance
 #align category_theory.locally_small CategoryTheory.LocallySmall
 
-instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] (X Y : C) : Small (X ⟶ Y) :=
+instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] (X Y : C) : Small.{w, v} (X ⟶ Y) :=
   LocallySmall.hom_small X Y
 
 theorem locallySmall_of_faithful {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]

Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean

@@ -51,7 +51,7 @@ instance hasFiniteLimits {B : C} [HasFiniteWidePullbacks C] : HasFiniteLimits (O
     exact ConstructProducts.over_binaryProduct_of_pullback
 #align category_theory.over.has_finite_limits CategoryTheory.Over.hasFiniteLimits
 
-instance hasLimits {B : C} [HasWidePullbacks.{w} C] : HasLimitsOfSize.{w} (Over B) := by
+instance hasLimits {B : C} [HasWidePullbacks.{w} C] : HasLimitsOfSize.{w, w} (Over B) := by
   apply @has_limits_of_hasEqualizers_and_products _ _ ?_ ?_
   · exact ConstructProducts.over_products_of_widePullbacks
   · apply @hasEqualizers_of_hasPullbacks_and_binary_products _ _ ?_ _

Mathlib/CategoryTheory/Sites/Adjunction.lean

@@ -20,10 +20,10 @@ namespace CategoryTheory
 
 open GrothendieckTopology CategoryTheory Limits Opposite
 
-universe v u
+universe v₁ v₂ u₁ u₂
 
-variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
-variable {D : Type*} [Category D]
+variable {C : Type u₁} [Category.{v₁} C] (J : GrothendieckTopology C)
+variable {D : Type u₂} [Category.{v₂} D]
 variable {E : Type*} [Category E]
 variable {F : D ⥤ E} {G : E ⥤ D}
 variable [HasWeakSheafify J D]
@@ -119,21 +119,21 @@ section ForgetToType
 variable [ConcreteCategory D] [HasSheafCompose J (forget D)]
 
 /-- This is the functor sending a sheaf of types `X` to the sheafification of `X ⋙ G`. -/
-abbrev composeAndSheafifyFromTypes (G : Type max v u ⥤ D) : SheafOfTypes J ⥤ Sheaf J D :=
+abbrev composeAndSheafifyFromTypes (G : Type max v₁ u₁ ⥤ D) : SheafOfTypes J ⥤ Sheaf J D :=
   (sheafEquivSheafOfTypes J).inverse ⋙ composeAndSheafify _ G
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.compose_and_sheafify_from_types CategoryTheory.Sheaf.composeAndSheafifyFromTypes
 
 /-- A variant of the adjunction between sheaf categories, in the case where the right adjoint
 is the forgetful functor to sheaves of types. -/
-def adjunctionToTypes {G : Type max v u ⥤ D} (adj : G ⊣ forget D) :
+def adjunctionToTypes {G : Type max v₁ u₁ ⥤ D} (adj : G ⊣ forget D) :
     composeAndSheafifyFromTypes J G ⊣ sheafForget J :=
   (sheafEquivSheafOfTypes J).symm.toAdjunction.comp (adjunction J adj)
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.adjunction_to_types CategoryTheory.Sheaf.adjunctionToTypes
 
 @[simp]
-theorem adjunctionToTypes_unit_app_val {G : Type max v u ⥤ D} (adj : G ⊣ forget D)
+theorem adjunctionToTypes_unit_app_val {G : Type max v₁ u₁ ⥤ D} (adj : G ⊣ forget D)
     (Y : SheafOfTypes J) :
     ((adjunctionToTypes J adj).unit.app Y).val =
       (adj.whiskerRight _).unit.app ((sheafOfTypesToPresheaf J).obj Y) ≫
@@ -145,7 +145,7 @@ set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.adjunction_to_types_unit_app_val CategoryTheory.Sheaf.adjunctionToTypes_unit_app_val
 
 @[simp]
-theorem adjunctionToTypes_counit_app_val {G : Type max v u ⥤ D} (adj : G ⊣ forget D)
+theorem adjunctionToTypes_counit_app_val {G : Type max v₁ u₁ ⥤ D} (adj : G ⊣ forget D)
     (X : Sheaf J D) :
     ((adjunctionToTypes J adj).counit.app X).val =
       sheafifyLift J ((Functor.associator _ _ _).hom ≫ (adj.whiskerRight _).counit.app _) X.2 := by
@@ -159,10 +159,7 @@ theorem adjunctionToTypes_counit_app_val {G : Type max v u ⥤ D} (adj : G ⊣ f
     NatIso.ofComponents, Adjunction.whiskerRight, Adjunction.mkOfUnitCounit]
   simp
 
-set_option linter.uppercaseLean3 false in
-#align category_theory.Sheaf.adjunction_to_types_counit_app_val CategoryTheory.Sheaf.adjunctionToTypes_counit_app_val
-
-instance [(forget D).IsRightAdjoint ] : (sheafForget J : Sheaf J D ⥤ _).IsRightAdjoint  :=
+instance [(forget D).IsRightAdjoint] : (sheafForget (D := D) J).IsRightAdjoint :=
   (adjunctionToTypes J (Adjunction.ofIsRightAdjoint (forget D))).isRightAdjoint
 
 end ForgetToType

Mathlib/CategoryTheory/Sites/Equivalence.lean

@@ -36,15 +36,15 @@ sufficiently small limits in the sheaf category on the essentially small site.
 
 -/
 
-universe u
+universe v₁ v₂ v₃ u₁ u₂ u₃ w
 
 namespace CategoryTheory
 
 open Functor Limits GrothendieckTopology
 
-variable {C : Type*} [Category C] (J : GrothendieckTopology C)
-variable {D : Type*} [Category D] (K : GrothendieckTopology D) (e : C ≌ D) (G : D ⥤ C)
-variable (A : Type*) [Category A]
+variable {C : Type u₁} [Category.{v₁} C] (J : GrothendieckTopology C)
+variable {D : Type u₂} [Category.{v₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (G : D ⥤ C)
+variable (A : Type u₃) [Category.{v₃} A]
 
 namespace Equivalence
 
@@ -213,7 +213,7 @@ theorem hasSheafCompose : J.HasSheafCompose F where
 
 end Equivalence
 
-variable [EssentiallySmall C]
+variable [EssentiallySmall.{w} C]
 variable (B : Type*) [Category B] (F : A ⥤ B)
 variable [HasSheafify ((equivSmallModel C).locallyCoverDense J).inducedTopology A]
 variable [((equivSmallModel C).locallyCoverDense J).inducedTopology.HasSheafCompose F]
@@ -239,13 +239,13 @@ instance hasSheafComposeEssentiallySmallSite : HasSheafCompose J F :=
 
 instance hasLimitsEssentiallySmallSite
     [HasLimits <| Sheaf ((equivSmallModel C).locallyCoverDense J).inducedTopology A] :
-    HasLimitsOfSize <| Sheaf J A :=
+    HasLimitsOfSize.{max v₃ w, max v₃ w} <| Sheaf J A :=
   Adjunction.has_limits_of_equivalence ((equivSmallModel C).sheafCongr J
     ((equivSmallModel C).locallyCoverDense J).inducedTopology A).functor
 
 instance hasColimitsEssentiallySmallSite
     [HasColimits <| Sheaf ((equivSmallModel C).locallyCoverDense J).inducedTopology A] :
-    HasColimitsOfSize <| Sheaf J A :=
+    HasColimitsOfSize.{max v₃ w, max v₃ w} <| Sheaf J A :=
   Adjunction.has_colimits_of_equivalence ((equivSmallModel C).sheafCongr J
     ((equivSmallModel C).locallyCoverDense J).inducedTopology A).functor
 

Mathlib/Condensed/Limits.lean

@@ -20,12 +20,14 @@ instance : HasLimits CondensedSet.{u} := by
   change HasLimits (Sheaf _ _)
   infer_instance
 
-instance : HasLimitsOfSize.{u} CondensedSet.{u} := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
+instance : HasLimitsOfSize.{u, u + 1} CondensedSet.{u} :=
+  hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
 
 variable (R : Type (u+1)) [Ring R]
 
 instance : HasLimits (CondensedMod.{u} R) := by
   change HasLimits (Sheaf _ _)
   infer_instance
 
-instance : HasLimitsOfSize.{u} (CondensedMod.{u} R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
+instance : HasLimitsOfSize.{u, u + 1} (CondensedMod.{u} R) :=
+  hasLimitsOfSizeShrink.{u, u+1, u+1, u} _

Mathlib/Data/Fintype/Prod.lean

@@ -76,7 +76,7 @@ theorem infinite_prod : Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨
   exact H'.false
 #align infinite_prod infinite_prod
 
-instance Pi.infinite_of_left {ι : Sort*} {π : ι → Sort _} [∀ i, Nontrivial <| π i] [Infinite ι] :
+instance Pi.infinite_of_left {ι : Sort*} {π : ι → Type*} [∀ i, Nontrivial <| π i] [Infinite ι] :
     Infinite (∀ i : ι, π i) := by
   choose m n hm using fun i => exists_pair_ne (π i)
   refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
@@ -85,25 +85,27 @@ instance Pi.infinite_of_left {ι : Sort*} {π : ι → Sort _} [∀ i, Nontrivia
 #align pi.infinite_of_left Pi.infinite_of_left
 
 /-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
-theorem Pi.infinite_of_exists_right {ι : Type*} {π : ι → Type*} (i : ι) [Infinite <| π i]
+theorem Pi.infinite_of_exists_right {ι : Sort*} {π : ι → Sort*} (i : ι) [Infinite <| π i]
     [∀ i, Nonempty <| π i] : Infinite (∀ i : ι, π i) :=
   let ⟨m⟩ := @Pi.instNonempty ι π _
   Infinite.of_injective _ (update_injective m i)
 #align pi.infinite_of_exists_right Pi.infinite_of_exists_right
 
 /-- See `Pi.infinite_of_exists_right` for the case that only one `π i` is infinite. -/
-instance Pi.infinite_of_right {ι : Sort _} {π : ι → Sort _} [∀ i, Infinite <| π i] [Nonempty ι] :
+instance Pi.infinite_of_right {ι : Sort*} {π : ι → Type*} [∀ i, Infinite <| π i] [Nonempty ι] :
     Infinite (∀ i : ι, π i) :=
   Pi.infinite_of_exists_right (Classical.arbitrary ι)
 #align pi.infinite_of_right Pi.infinite_of_right
 
 /-- Non-dependent version of `Pi.infinite_of_left`. -/
-instance Function.infinite_of_left {ι π : Sort _} [Nontrivial π] [Infinite ι] : Infinite (ι → π) :=
+instance Function.infinite_of_left {ι : Sort*} {π : Type*} [Nontrivial π] [Infinite ι] :
+    Infinite (ι → π) :=
   Pi.infinite_of_left
 #align function.infinite_of_left Function.infinite_of_left
 
 /-- Non-dependent version of `Pi.infinite_of_exists_right` and `Pi.infinite_of_right`. -/
-instance Function.infinite_of_right {ι π : Sort _} [Infinite π] [Nonempty ι] : Infinite (ι → π) :=
+instance Function.infinite_of_right {ι : Sort*} {π : Type*} [Infinite π] [Nonempty ι] :
+    Infinite (ι → π) :=
   Pi.infinite_of_right
 #align function.infinite_of_right Function.infinite_of_right
 

Mathlib/Geometry/RingedSpace/Basic.lean

@@ -37,7 +37,7 @@ namespace AlgebraicGeometry
 
 /-- The type of Ringed spaces, as an abbreviation for `SheafedSpace CommRingCat`. -/
 abbrev RingedSpace : TypeMax.{u+1, v+1} :=
-  SheafedSpace.{_, v, u} CommRingCat.{v}
+  SheafedSpace.{v+1, v, u} CommRingCat.{v}
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.RingedSpace AlgebraicGeometry.RingedSpace
 

Mathlib/Geometry/RingedSpace/SheafedSpace.lean

@@ -21,7 +21,10 @@ presheaves.
 open CategoryTheory TopCat TopologicalSpace Opposite CategoryTheory.Limits CategoryTheory.Category
   CategoryTheory.Functor
 
-variable (C : Type*) [Category C]
+universe u v
+
+variable (C : Type u) [Category.{v} C]
+
 
 -- Porting note: removed
 -- local attribute [tidy] tactic.op_induction'
@@ -251,7 +254,7 @@ noncomputable instance [HasLimits C] :
           limit_isSheaf _ fun j => Sheaf.pushforward_sheaf_of_sheaf _ (K.obj (unop j)).2⟩
         (colimit.isoColimitCocone ⟨_, PresheafedSpace.colimitCoconeIsColimit _⟩).symm⟩⟩
 
-instance [HasLimits C] : HasColimits (SheafedSpace C) :=
+instance [HasLimits C] : HasColimits.{v} (SheafedSpace C) :=
   hasColimits_of_hasColimits_createsColimits forgetToPresheafedSpace
 
 noncomputable instance [HasLimits C] : PreservesColimits (forget C) :=

Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

@@ -296,8 +296,9 @@ instance generators_connected (G) [Groupoid.{u, u} G] [IsConnected G] [IsFreeGro
 
 /-- A vertex group in a free connected groupoid is free. With some work one could drop the
 connectedness assumption, by looking at connected components. -/
-instance endIsFreeOfConnectedFree {G} [Groupoid G] [IsConnected G] [IsFreeGroupoid G] (r : G) :
-    IsFreeGroup (End r) :=
+instance endIsFreeOfConnectedFree
+    {G : Type u} [Groupoid G] [IsConnected G] [IsFreeGroupoid G] (r : G) :
+    IsFreeGroup.{u} (End r) :=
   SpanningTree.endIsFree <| geodesicSubtree (symgen r)
 #align is_free_groupoid.End_is_free_of_connected_free IsFreeGroupoid.endIsFreeOfConnectedFree
 

Mathlib/Logic/Equiv/Basic.lean

@@ -1976,7 +1976,7 @@ end
 
 section BinaryOp
 
-variable (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)
+variable {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)
 
 theorem semiconj_conj (f : α₁ → α₁) : Semiconj e f (e.conj f) := fun x => by simp
 #align equiv.semiconj_conj Equiv.semiconj_conj