[Merged by Bors] - chore: adaptation for batteries#1864 and batteries#1866

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -99,12 +99,6 @@ abbrev of (V : Type v) [AddCommGroup V] [Module R V] [Module.Finite R V] : FGMod
 lemma of_carrier (V : Type v) [AddCommGroup V] [Module R V] [Module.Finite R V] :
     of R V = V := rfl
 
-/-
-The reduction done by `simpVarHead` is stronger than the one actually used by `simp`,
-so we get a false positive here
--/
-attribute [nolint simpVarHead] of_carrier
-
 variable {R} in
 /-- Lift a linear map between finitely generated modules to `FGModuleCat R`. -/
 abbrev ofHom {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V]

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -602,22 +602,20 @@ instance CommGrpCat.forget_reflects_isos : (forget CommGrpCat.{u}).ReflectsIsomo
 -- this variant is then renamed with an `Aux` suffix
 set_option linter.checkUnivs false in
 /-- An alias for `GrpCat.{max u v}`, to deal around unification issues. -/
-@[to_additive (attr := nolint checkUnivs) GrpMaxAux
+@[to_additive GrpMaxAux
   /-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues. -/]
 abbrev GrpMax.{u1, u2} := GrpCat.{max u1 u2}
 
 set_option linter.checkUnivs false in
 /-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues. -/
-@[nolint checkUnivs]
 abbrev AddGrpMax.{u1, u2} := AddGrpCat.{max u1 u2}
 
 set_option linter.checkUnivs false in
 /-- An alias for `CommGrpCat.{max u v}`, to deal around unification issues. -/
-@[to_additive (attr := nolint checkUnivs) AddCommGrpMaxAux
+@[to_additive AddCommGrpMaxAux
   /-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues. -/]
 abbrev CommGrpMax.{u1, u2} := CommGrpCat.{max u1 u2}
 
 set_option linter.checkUnivs false in
 /-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues. -/
-@[nolint checkUnivs]
 abbrev AddCommGrpMax.{u1, u2} := AddCommGrpCat.{max u1 u2}

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -52,7 +52,6 @@ set_option linter.checkUnivs false in
 /-- Given a ring `A`, this structure involves a family of elements (indexed by a type `R`)
 in a free module `G →₀ A`. This allows to define an `A`-module by generators and relations,
 see `Relations.Quotient`. -/
-@[nolint checkUnivs]
 structure Relations where
   /-- the index type for generators -/
   G : Type w₀
@@ -492,7 +491,6 @@ variable (M : Type v) [AddCommGroup M] [Module A M]
 set_option linter.checkUnivs false in
 /-- Given an `A`-module `M`, a term in this type is a presentation by `M` by
 generators and relations. -/
-@[nolint checkUnivs]
 structure Presentation extends Relations.{w₀, w₁} A,
   toRelations.Solution M, toSolution.IsPresentation where
 

Mathlib/CategoryTheory/Bicategory/Basic.lean

@@ -58,7 +58,6 @@ These associators and unitors satisfy the pentagon and triangle equations.
 
 See https://ncatlab.org/nlab/show/bicategory.
 -/
-@[nolint checkUnivs]
 class Bicategory (B : Type u) extends CategoryStruct.{v} B where
   /-- The category structure on the collection of 1-morphisms -/
   homCategory : ∀ a b : B, Category.{w} (a ⟶ b) := by infer_instance

Mathlib/CategoryTheory/Category/Cat.lean

@@ -33,7 +33,6 @@ open Bicategory Functor
 -- intended to be used with explicit universe parameters
 set_option linter.checkUnivs false in
 /-- Category of categories. -/
-@[nolint checkUnivs]
 def Cat :=
   Bundled Category.{v, u}
 

Mathlib/CategoryTheory/Category/Quiv.lean

@@ -24,7 +24,6 @@ namespace CategoryTheory
 -- intended to be used with explicit universe parameters
 set_option linter.checkUnivs false in
 /-- Category of quivers. -/
-@[nolint checkUnivs]
 def Quiv :=
   Bundled Quiver.{v, u}
 

Mathlib/CategoryTheory/Category/ReflQuiv.lean

@@ -23,7 +23,6 @@ universe v u v₁ v₂ u₁ u₂
 
 set_option linter.checkUnivs false in
 /-- Category of refl quivers. -/
-@[nolint checkUnivs]
 def ReflQuiv :=
   Bundled ReflQuiver.{v, u}
 

Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean

@@ -38,7 +38,6 @@ variable {𝒮 : Type u₁} [Category.{v₁} 𝒮]
 
 set_option linter.checkUnivs false in
 /-- A based category over `𝒮` is a category `𝒳` together with a functor `p : 𝒳 ⥤ 𝒮`. -/
-@[nolint checkUnivs]
 structure BasedCategory (𝒮 : Type u₁) [Category.{v₁} 𝒮] where
   /-- The type of objects in a `BasedCategory` -/
   obj : Type u₂

Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean

@@ -63,7 +63,6 @@ set_option linter.checkUnivs false in
 collection of categories `Fib S` for every `S : 𝒮` (the fiber categories), each equipped with a
 functors `ι : Fib S ⥤ 𝒳` which map constantly to `S` on the base such that the induced functor
 `Fib S ⥤ Fiber p S` is an equivalence. -/
-@[nolint checkUnivs]
 class HasFibers (p : 𝒳 ⥤ 𝒮) where
   /-- The type of objects of the category `Fib S` for each `S`. -/
   Fib (S : 𝒮) : Type u₃

Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean

@@ -35,7 +35,6 @@ namespace CategoryTheory
 -- intended to be used with explicit universe parameters
 set_option linter.checkUnivs false in
 /-- Category of groupoids -/
-@[nolint checkUnivs]
 def Grpd :=
   Bundled Groupoid.{v, u}
 

Mathlib/CategoryTheory/Limits/Chosen/End.lean

@@ -32,7 +32,7 @@ class ChosenCoendsOfShape (J : Type*) [Category* J] (C : Type*) [Category* C] wh
 
 set_option linter.checkUnivs false in
 /-- The data of chosen coends in `C`. -/
-@[nolint checkUnivs, pp_with_univ]
+@[pp_with_univ]
 abbrev ChosenCoends (C : Type*) [Category* C] :=
   ∀ {J : Type u} [Category.{v} J], ChosenCoendsOfShape J C
 
@@ -107,7 +107,7 @@ class ChosenEndsOfShape (J : Type*) [Category* J] (C : Type*) [Category* C] wher
 
 set_option linter.checkUnivs false in
 /-- The data of chosen ends in `C`. -/
-@[nolint checkUnivs, pp_with_univ]
+@[pp_with_univ]
 abbrev ChosenEnds (C : Type*) [Category* C] :=
   ∀ {J : Type u} [Category.{v} J], ChosenEndsOfShape J C
 

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -87,7 +87,7 @@ set_option linter.checkUnivs false in
 -- https://github.com/leanprover/lean4/pull/12423, the shape universes in
 -- `CreatesLimitsOfSize` and `CreatesColimitsOfSize` would default to universe output parameters.
 -- See Note [universe output parameters and typeclass caching].
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class CreatesLimitsOfSize (F : C ⥤ D) where
   CreatesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], CreatesLimitsOfShape J F := by
     infer_instance
@@ -117,7 +117,7 @@ class CreatesColimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) where
 -- This should be used with explicit universe variables.
 set_option linter.checkUnivs false in
 /-- `F` creates colimits if it creates colimits of shape `J` for any small `J`. -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class CreatesColimitsOfSize (F : C ⥤ D) where
   CreatesColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], CreatesColimitsOfShape J F := by
     infer_instance

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -80,7 +80,7 @@ diagram `J ⥤ C` to limit cones, where `J : Type u` with `[Category.{v} J]`. -/
 -- `PreservesLimitsOfSize`, `PreservesColimitsOfSize`, `ReflectsLimitsOfSize`, and
 -- `ReflectsColimitsOfSize` would default to universe output parameters.
 -- See Note [universe output parameters and typeclass caching].
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class PreservesLimitsOfSize (F : C ⥤ D) : Prop where
   preservesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], PreservesLimitsOfShape J F := by
     infer_instance
@@ -93,7 +93,7 @@ abbrev PreservesLimits (F : C ⥤ D) :=
 -- This should be used with explicit universe variables.
 /-- `PreservesColimitsOfSize.{v u} F` means that `F` sends all colimit cocones over any
 diagram `J ⥤ C` to colimit cocones, where `J : Type u` with `[Category.{v} J]`. -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class PreservesColimitsOfSize (F : C ⥤ D) : Prop where
   preservesColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], PreservesColimitsOfShape J F := by
     infer_instance
@@ -415,7 +415,7 @@ whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone i
 the cone was already a limit cone in `C`.
 Note that we do not assume a priori that `D` actually has any limits.
 -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class ReflectsLimitsOfSize (F : C ⥤ D) : Prop where
   reflectsLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], ReflectsLimitsOfShape J F := by
     infer_instance
@@ -434,7 +434,7 @@ whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit co
 the cocone was already a colimit cocone in `C`.
 Note that we do not assume a priori that `D` actually has any colimits.
 -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class ReflectsColimitsOfSize (F : C ⥤ D) : Prop where
   reflectsColimitsOfShape : ∀ {J : Type w} [Category.{w'} J], ReflectsColimitsOfShape J F := by
     infer_instance

Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean

@@ -48,7 +48,7 @@ filtered diagram `J ⥤ C` to colimit cocones, where `J : Type w` with `[Categor
 -- `PreservesFilteredColimitsOfSize`, `ReflectsFilteredColimitsOfSize`,
 -- `PreservesCofilteredLimitsOfSize`, and `ReflectsCofilteredLimitsOfSize` would default to
 -- universe output parameters. See Note [universe output parameters and typeclass caching].
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class PreservesFilteredColimitsOfSize (F : C ⥤ D) : Prop where
   preserves_filtered_colimits :
     ∀ (J : Type w) [Category.{w'} J] [IsFiltered J], PreservesColimitsOfShape J F
@@ -104,7 +104,7 @@ section Reflects
 -- This should be used with explicit universe variables.
 /-- `ReflectsFilteredColimitsOfSize.{w', w} F` means that whenever the image of a filtered cocone
 under `F` is a colimit cocone, the original cocone was already a colimit. -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class ReflectsFilteredColimitsOfSize (F : C ⥤ D) : Prop where
   reflects_filtered_colimits :
     ∀ (J : Type w) [Category.{w'} J] [IsFiltered J], ReflectsColimitsOfShape J F
@@ -164,7 +164,7 @@ section Preserves
 -- This should be used with explicit universe variables.
 /-- `PreservesCofilteredLimitsOfSize.{w', w} F` means that `F` sends all limit cones over any
 cofiltered diagram `J ⥤ C` to limit cones, where `J : Type w` with `[Category.{w'} J]`. -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class PreservesCofilteredLimitsOfSize (F : C ⥤ D) : Prop where
   preserves_cofiltered_limits :
     ∀ (J : Type w) [Category.{w'} J] [IsCofiltered J], PreservesLimitsOfShape J F
@@ -220,7 +220,7 @@ section Reflects
 -- This should be used with explicit universe variables.
 /-- `ReflectsCofilteredLimitsOfSize.{w', w} F` means that whenever the image of a cofiltered cone
 under `F` is a limit cone, the original cone was already a limit. -/
-@[univ_out_params, nolint checkUnivs, pp_with_univ]
+@[univ_out_params, pp_with_univ]
 class ReflectsCofilteredLimitsOfSize (F : C ⥤ D) : Prop where
   reflects_cofiltered_limits :
     ∀ (J : Type w) [Category.{w'} J] [IsCofiltered J], ReflectsLimitsOfShape J F

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -38,7 +38,6 @@ universe t w w' v u
 set_option linter.checkUnivs false in
 /-- The shape of a multiequalizer diagram. It involves two types `L` and `R`,
 and two maps `R → L`. -/
-@[nolint checkUnivs]
 structure MulticospanShape where
   /-- the left type -/
   L : Type w
@@ -62,7 +61,6 @@ def MulticospanShape.prod (ι : Type w) : MulticospanShape where
 set_option linter.checkUnivs false in
 /-- The shape of a multicoequalizer diagram. It involves two types `L` and `R`,
 and two maps `L → R`. -/
-@[nolint checkUnivs]
 structure MultispanShape where
   /-- the left type -/
   L : Type w
@@ -300,7 +298,6 @@ def arrowEquiv :
 end WalkingMultispan
 
 /-- This is a structure encapsulating the data necessary to define a `Multicospan`. -/
-@[nolint checkUnivs]
 structure MulticospanIndex (J : MulticospanShape.{w, w'})
     (C : Type u) [Category.{v} C] where
   /-- Left map, from `J.L` to `C` -/
@@ -313,7 +310,6 @@ structure MulticospanIndex (J : MulticospanShape.{w, w'})
   snd : ∀ b, left (J.snd b) ⟶ right b
 
 /-- This is a structure encapsulating the data necessary to define a `Multispan`. -/
-@[nolint checkUnivs]
 structure MultispanIndex (J : MultispanShape.{w, w'})
     (C : Type u) [Category.{v} C] where
   /-- Left map, from `J.L` to `C` -/

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

@@ -168,7 +168,7 @@ structure Hom (X Y : P.Comma L R Q W) extends CommaMorphism X.toComma Y.toComma
 abbrev Hom.hom {X Y : P.Comma L R Q W} (f : Comma.Hom X Y) : X.toComma ⟶ Y.toComma :=
   f.toCommaMorphism
 
-@[simp, nolint simpVarHead]
+@[simp]
 lemma Hom.hom_mk {X Y : P.Comma L R Q W} (f : CommaMorphism X.toComma Y.toComma) (hf) (hg) :
     Comma.Hom.hom ⟨f, hf, hg⟩ = f := rfl
 

Mathlib/Data/PFunctor/Univariate/Basic.lean

@@ -18,6 +18,8 @@ This file defines polynomial functors and the W-type construction as a polynomia
 
 universe u v uA uB uA₁ uB₁ uA₂ uB₂ v₁ v₂ v₃
 
+-- Note: `set_option linter.checkUnivs` should not apply here,
+-- we really do want two separate universe levels
 set_option linter.checkUnivs false in
 /-- A polynomial functor `P` is given by a type `A` and a family `B` of types over `A`. `P` maps
 any type `α` to a new type `P α`, which is defined as the sigma type `Σ x, P.B x → α`.
@@ -26,8 +28,7 @@ An element of `P α` is a pair `⟨a, f⟩`, where `a` is an element of a type `
 `f : B a → α`. Think of `a` as the shape of the object and `f` as an index to the relevant
 elements of `α`.
 -/
--- Note: `nolint checkUnivs` should not apply here, we really do want two separate universe levels
-@[pp_with_univ, nolint checkUnivs]
+@[pp_with_univ]
 structure PFunctor where
   /-- The head type -/
   A : Type uA

Mathlib/Geometry/RingedSpace/Basic.lean

@@ -38,9 +38,9 @@ open TopCat.Presheaf
 
 namespace AlgebraicGeometry
 
+-- The universes appear together in the type, but separately in the value.
 set_option linter.checkUnivs false in
 /-- The type of Ringed spaces, as an abbreviation for `SheafedSpace CommRingCat`. -/
-@[nolint checkUnivs] -- The universes appear together in the type, but separately in the value.
 abbrev RingedSpace : Type max (u + 1) (v + 1) :=
   SheafedSpace.{v + 1, v, u} CommRingCat.{v}
 

Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

@@ -84,7 +84,7 @@ structure Hom (X Y : LocallyRingedSpace.{u}) : Type _
 abbrev Hom.toShHom {X Y : LocallyRingedSpace.{u}} (f : X.Hom Y) :
   X.toSheafedSpace ⟶ Y.toSheafedSpace := InducedCategory.homMk f.1
 
-@[simp, nolint simpVarHead]
+@[simp]
 lemma Hom.toShHom_mk {X Y : LocallyRingedSpace.{u}}
     (f : X.toPresheafedSpace.Hom Y.toPresheafedSpace) (hf) :
   Hom.toShHom ⟨f, hf⟩ = InducedCategory.homMk f := rfl

Mathlib/ModelTheory/Basic.lean

@@ -55,7 +55,6 @@ namespace FirstOrder
 set_option linter.checkUnivs false in
 /-- A first-order language consists of a type of functions of every natural-number arity and a
   type of relations of every natural-number arity. -/
-@[nolint checkUnivs]
 structure Language where
   /-- For every arity, a `Type u` of functions of that arity -/
   Functions : ℕ → Type u

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -55,7 +55,6 @@ A presentation of an `R`-algebra `S` is a family of
 generators with `σ → MvPolynomial ι R`: The assignment of
 each relation to a polynomial in the generators.
 -/
-@[nolint checkUnivs]
 structure Algebra.Presentation extends Algebra.Generators R S ι where
   /-- The assignment of each relation to a polynomial in the generators. -/
   relation : σ → toGenerators.Ring

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

@@ -64,7 +64,6 @@ with relations equipped with an injective `map : relations → vars`.
 This map determines how the differential of `P` is constructed. See
 `PreSubmersivePresentation.differential` for details.
 -/
-@[nolint checkUnivs]
 structure PreSubmersivePresentation extends Algebra.Presentation R S ι σ where
   /-- A map from the relations type to the variables type. Used to compute the differential. -/
   map : σ → ι
@@ -495,7 +494,6 @@ variable [Finite σ]
 A `PreSubmersivePresentation` is submersive if its Jacobian is a unit in `S`
 and the presentation is finite.
 -/
-@[nolint checkUnivs]
 structure SubmersivePresentation extends PreSubmersivePresentation.{t, w} R S ι σ where
   jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian
 

Mathlib/SetTheory/Ordinal/Univ.lean

@@ -33,7 +33,7 @@ open Ordinal in
 -- intended to be used with explicit universe parameters
 /-- The ordinal `univ.{u, v}` is the order type of `Ordinal.{u}` or `Cardinal.{u}`, as an element of
 `Ordinal.{v}` (when `u < v`). -/
-@[pp_with_univ, nolint checkUnivs]
+@[pp_with_univ]
 def Ordinal.univ : Ordinal.{max (u + 1) v} :=
   lift.{v, u + 1} (typeLT Ordinal)
 
@@ -42,7 +42,7 @@ open Cardinal in
 -- intended to be used with explicit universe parameters
 /-- The cardinal `univ.{u, v}` is the cardinality of `Ordinal.{u}` or `Cardinal.{u}`, as an element
 of `Cardinal.{v}` (when `u < v`). -/
-@[pp_with_univ, nolint checkUnivs]
+@[pp_with_univ]
 def Cardinal.univ : Cardinal.{max (u + 1) v} :=
   lift.{v, u + 1} #Ordinal
 

Mathlib/SetTheory/ZFC/PSet.lean

@@ -443,7 +443,6 @@ protected def Lift : PSet.{u} → PSet.{max u v}
 -- intended to be used with explicit universe parameters
 set_option linter.checkUnivs false in
 /-- Embedding of one universe in another -/
-@[nolint checkUnivs]
 def embed : PSet.{max (u + 1) v} :=
   ⟨ULift.{v, u + 1} PSet, fun ⟨x⟩ => PSet.Lift.{u, max (u + 1) v} x⟩
 

Mathlib/Topology/Category/CompHausLike/Limits.lean

@@ -120,6 +120,11 @@ lemma finiteCoproduct.ι_desc_apply {B : CompHausLike P} {π : (a : α) → X a
 instance : HasCoproduct X where
   exists_colimit := ⟨finiteCoproduct.cofan X, finiteCoproduct.isColimit X⟩
 
+/-
+This linter complains that the universes `u` and `w` only occur together, but `w` appears by itself
+in the indexing type of the coproduct. In almost all cases, `w` will be either `0` or `u`, but we
+want to allow both possibilities.
+-/
 set_option linter.checkUnivs false in
 variable (P) in
 /--
@@ -129,13 +134,6 @@ property `P`.
 class HasExplicitFiniteCoproducts : Prop where
   hasProp {α : Type w} [Finite α] (X : α → CompHausLike.{max u w} P) : HasExplicitFiniteCoproduct X
 
-/-
-This linter complains that the universes `u` and `w` only occur together, but `w` appears by itself
-in the indexing type of the coproduct. In almost all cases, `w` will be either `0` or `u`, but we
-want to allow both possibilities.
--/
-attribute [nolint checkUnivs] HasExplicitFiniteCoproducts
-
 attribute [instance] HasExplicitFiniteCoproducts.hasProp
 
 instance [HasExplicitFiniteCoproducts.{w} P] (α : Type w) [Finite α] :

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "125807f43a86b5d58892b7ea6972eec0d6c164d2",
+   "rev": "e535e4feb0aa360e59e7adf4837b91ffbfb8c943",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",