convert #adaptation_note to -- comments for univ_out_params annotations

kim-em · claude · kim-em · commit 082d63c4e875 · 2026-02-15T13:39:53.000+11:00
These are permanent annotations, not temporary workarounds, so
#adaptation_note is the wrong mechanism. Use regular comments placed
after the doc-string and before the @[univ_out_params] attribute.

Also restore the reference to lean4#12423 alongside lean4#12286.

Co-Authored-By: Claude Opus 4.6 &lt;noreply@anthropic.com&gt;
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -222,12 +222,13 @@ elab (name := cat_disch) "cat_disch" : tactic =>
 
 set_option mathlib.tactic.category.grind true
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the morphism universe `v` would default to being a universe output parameter.
-See Note [universe output parameters and typeclass caching]. -/
 /-- The typeclass `Category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `Category.{v} C`. (See also `LargeCategory` and `SmallCategory`.) -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the morphism universe `v` would default to
+-- being a universe output parameter.
+-- See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ, stacks 0014]
 class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
   /-- Identity morphisms are left identities for composition. -/
diff --git a/Mathlib/CategoryTheory/Enriched/Limits/HasConicalLimits.lean b/Mathlib/CategoryTheory/Enriched/Limits/HasConicalLimits.lean
@@ -68,13 +68,13 @@ class HasConicalLimitsOfShape : Prop where
 
 attribute [instance] HasConicalLimitsOfShape.hasConicalLimit
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes `v₁, u₁` would default to universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 /--
 `C` has all conical limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
 if it has conical limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes `v₁, u₁` would default
+-- to universe output parameters. See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ]
 class HasConicalLimitsOfSize : Prop where
   /-- All functors `F : J ⥤ C` from all small `J` have conical limits -/
diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -36,12 +36,12 @@ variable (C : Type u) [Category.{v} C]
 
 namespace CategoryTheory
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the smallness universe `w` in `EssentiallySmall` and `LocallySmall` would default to a
-universe output parameter.
-See Note [universe output parameters and typeclass caching]. -/
 /-- A category is `EssentiallySmall.{w}` if there exists
 an equivalence to some `S : Type w` with `[SmallCategory S]`. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the smallness universe `w` in
+-- `EssentiallySmall` and `LocallySmall` would default to a universe output parameter.
+-- See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ]
 class EssentiallySmall (C : Type u) [Category.{v} C] : Prop where
   /-- An essentially small category is equivalent to some small category. -/
@@ -92,6 +92,7 @@ theorem essentiallySmallSelf : EssentiallySmall.{max w v u} C :=
 
 See `ShrinkHoms C` for a category instance where every hom set has been replaced by a small model.
 -/
+-- See comment on `EssentiallySmall` above.
 @[univ_out_params, pp_with_univ]
 class LocallySmall (C : Type u) [Category.{v} C] : Prop where
   /-- A locally small category has small hom-types. -/
diff --git a/Mathlib/CategoryTheory/Limits/Creates.lean b/Mathlib/CategoryTheory/Limits/Creates.lean
@@ -80,12 +80,12 @@ class CreatesLimit (K : J ⥤ C) (F : C ⥤ D) extends ReflectsLimit K F where
 class CreatesLimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) where
   CreatesLimit : ∀ {K : J ⥤ C}, CreatesLimit K F := by infer_instance
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes in `CreatesLimitsOfSize` and `CreatesColimitsOfSize` would default to
-universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 -- This should be used with explicit universe variables.
 /-- `F` creates limits if it creates limits of shape `J` for any `J`. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- 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]
 class CreatesLimitsOfSize (F : C ⥤ D) where
   CreatesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], CreatesLimitsOfShape J F := by
diff --git a/Mathlib/CategoryTheory/Limits/Filtered.lean b/Mathlib/CategoryTheory/Limits/Filtered.lean
@@ -69,11 +69,11 @@ section
 
 variable (C)
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes in `HasCofilteredLimitsOfSize` and `HasFilteredColimitsOfSize` would default
-to universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 /-- Class for having all cofiltered limits of a given size. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes in
+-- `HasCofilteredLimitsOfSize` and `HasFilteredColimitsOfSize` would default to universe
+-- output parameters. See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ]
 class HasCofilteredLimitsOfSize : Prop where
   /-- For all filtered types of size `w`, we have limits -/
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -101,12 +101,12 @@ class HasLimitsOfShape : Prop where
   /-- All functors `F : J ⥤ C` from `J` have limits -/
   has_limit : ∀ F : J ⥤ C, HasLimit F := by infer_instance
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes `v₁, u₁` would default to universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 /-- `C` has all limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
 if it has limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes `v₁, u₁` would default
+-- to universe output parameters. See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ]
 class HasLimitsOfSize (C : Type u) [Category.{v} C] : Prop where
   /-- All functors `F : J ⥤ C` from all small `J` have limits -/
@@ -626,12 +626,12 @@ class HasColimitsOfShape : Prop where
   /-- All `F : J ⥤ C` have colimits for a fixed `J` -/
   has_colimit : ∀ F : J ⥤ C, HasColimit F := by infer_instance
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes `v₁, u₁` would default to universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 /-- `C` has all colimits of size `v₁ u₁` (`HasColimitsOfSize.{v₁ u₁} C`)
 if it has colimits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes `v₁, u₁` would default
+-- to universe output parameters. See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ]
 class HasColimitsOfSize (C : Type u) [Category.{v} C] : Prop where
   /-- All `F : J ⥤ C` have colimits for all small `J` -/
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -72,13 +72,14 @@ class PreservesLimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop
 class PreservesColimitsOfShape (J : Type w) [Category.{w'} J] (F : C ⥤ D) : Prop where
   preservesColimit : ∀ {K : J ⥤ C}, PreservesColimit K F := by infer_instance
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes `w, w'` in `PreservesLimitsOfSize`, `PreservesColimitsOfSize`,
-`ReflectsLimitsOfSize`, and `ReflectsColimitsOfSize` would default to universe output
-parameters. See Note [universe output parameters and typeclass caching]. -/
 -- This should be used with explicit universe variables.
 /-- `PreservesLimitsOfSize.{v u} F` means that `F` sends all limit cones over any
 diagram `J ⥤ C` to limit cones, where `J : Type u` with `[Category.{v} J]`. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes `w, w'` in
+-- `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]
 class PreservesLimitsOfSize (F : C ⥤ D) : Prop where
   preservesLimitsOfShape : ∀ {J : Type w} [Category.{w'} J], PreservesLimitsOfShape J F := by
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean b/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
@@ -40,14 +40,14 @@ section FilteredColimits
 
 section Preserves
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the shape universes in `PreservesFilteredColimitsOfSize`, `ReflectsFilteredColimitsOfSize`,
-`PreservesCofilteredLimitsOfSize`, and `ReflectsCofilteredLimitsOfSize` would default to
-universe output parameters.
-See Note [universe output parameters and typeclass caching]. -/
 -- This should be used with explicit universe variables.
 /-- `PreservesFilteredColimitsOfSize.{w', w} F` means that `F` sends all colimit cocones over any
 filtered diagram `J ⥤ C` to colimit cocones, where `J : Type w` with `[Category.{w'} J]`. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the shape universes in
+-- `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]
 class PreservesFilteredColimitsOfSize (F : C ⥤ D) : Prop where
   preserves_filtered_colimits :
diff --git a/Mathlib/CategoryTheory/Localization/SmallHom.lean b/Mathlib/CategoryTheory/Localization/SmallHom.lean
@@ -40,12 +40,12 @@ section
 
 variable (L : C ⥤ D) [L.IsLocalization W] (X Y Z : C)
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the universe `w` would default to a universe output parameter.
-See Note [universe output parameters and typeclass caching]. -/
 /-- This property holds if the type of morphisms between `X` and `Y`
 in the localized category with respect to `W : MorphismProperty C`
 is small. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the universe `w` would default to a
+-- universe output parameter. See Note [universe output parameters and typeclass caching].
 @[univ_out_params]
 class HasSmallLocalizedHom : Prop where
   small : Small.{w} (W.Q.obj X ⟶ W.Q.obj Y)
diff --git a/Mathlib/CategoryTheory/Sites/Continuous.lean b/Mathlib/CategoryTheory/Sites/Continuous.lean
@@ -118,12 +118,12 @@ variable (F F' : C ⥤ D) (τ : F ⟶ F') (e : F ≅ F') (G : D ⥤ E)
 abbrev PreservesOneHypercovers :=
   ∀ {X : C} (E : GrothendieckTopology.OneHypercover.{w} J X), E.IsPreservedBy F K
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the sheaf type universe `t` would default to a universe output parameter,
-causing failures when a lemma needs `IsContinuous` at two different universe levels.
-See Note [universe output parameters and typeclass caching]. -/
 /-- A functor `F` is continuous if the precomposition with `F.op` sends sheaves of `Type t`
 to sheaves. -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the sheaf type universe `t` would default
+-- to a universe output parameter, causing failures when a lemma needs `IsContinuous` at two
+-- different universe levels. See Note [universe output parameters and typeclass caching].
 @[univ_out_params]
 class IsContinuous : Prop where
   op_comp_isSheaf_of_types (G : Sheaf K (Type t)) : Presieve.IsSheaf J (F.op ⋙ G.val)
diff --git a/Mathlib/Logic/Small/Defs.lean b/Mathlib/Logic/Small/Defs.lean
@@ -27,13 +27,12 @@ See `Mathlib/Logic/Small/Basic.lean` for further instances and theorems.
 
 universe u w v v'
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the type universe `v` of `α` would default to a universe output parameter.
-Marking `v` as output is actually correct here (it *is* determined by `α`), but we still
-need the attribute to prevent `w` from also being treated as output.
-See Note [universe output parameters and typeclass caching]. -/
 /-- A type is `Small.{w}` if there exists an equivalence to some `S : Type w`.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423: `v` is a true output (determined by `α`),
+-- but we need the attribute to prevent `w` from also being treated as output.
+-- See Note [universe output parameters and typeclass caching].
 @[univ_out_params v, mk_iff, pp_with_univ]
 class Small (α : Type v) : Prop where
   /-- If a type is `Small.{w}`, then there exists an equivalence with some `S : Type w` -/
diff --git a/Mathlib/Logic/UnivLE.lean b/Mathlib/Logic/UnivLE.lean
@@ -25,10 +25,6 @@ universe u v w
 
 noncomputable section
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-both universe parameters of `UnivLE` would default to universe output parameters
-(since it has no input parameters at all).
-See Note [universe output parameters and typeclass caching]. -/
 /--
 A class expressing a universe inequality. `UnivLE.{u, v}` expresses that `u ≤ v`.
 
@@ -45,6 +41,10 @@ it could be bigger than both!
 See also `Mathlib/CategoryTheory/UnivLE.lean` for the statement that the stronger definition is
 equivalent to `EssSurj (uliftFunctor : Type v ⥤ Type max u v)`.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, both universe parameters would default to
+-- output (since there are no input parameters at all).
+-- See Note [universe output parameters and typeclass caching].
 @[univ_out_params, pp_with_univ, mk_iff]
 class UnivLE : Prop where
   small (α : Type u) : Small.{v} α
diff --git a/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean b/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
@@ -71,9 +71,6 @@ lemma continuous_from_compactlyGenerated [TopologicalSpace X] [t : TopologicalSp
   rw [continuous_coinduced_dom]
   continuity
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12286,
-the compact space universe `u` would default to a universe output parameter.
-See Note [universe output parameters and typeclass caching]. -/
 /--
 A topological space `X` is compactly generated if its topology is finer than (and thus equal to)
 the compactly generated topology, i.e. it is coinduced by the continuous maps from compact
@@ -83,6 +80,9 @@ This version includes an explicit universe parameter `u` which should always be
 intended for categorical purposes. See `CompactlyGeneratedSpace` for the version without this
 parameter, intended for topological purposes.
 -/
+-- After https://github.com/leanprover/lean4/pull/12286 and
+-- https://github.com/leanprover/lean4/pull/12423, the compact space universe `u` would default
+-- to a universe output parameter. See Note [universe output parameters and typeclass caching].
 @[univ_out_params]
 class UCompactlyGeneratedSpace (X : Type v) [t : TopologicalSpace X] : Prop where
   /-- The topology of `X` is finer than the compactly generated topology. -/
