chore: ensure there is a replacement identifier or text suggestion fo…

…r all deprecations (#19426)

This is for compatibility with the stricter requirements of leanprover/lean4#6112.

Anyone is welcome to replace the "No deprecation message was provided." messages in other PRs! :-)

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -634,7 +634,7 @@ end MonoidHom
 end MonoidHom
 
 set_option linter.deprecated false in
-@[simp, deprecated (since := "2024-10-17")]
+@[simp, deprecated "No deprecation message was provided." (since := "2024-10-17")]
 lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum := rfl
 
 namespace List

Mathlib/Algebra/Group/Action/Defs.lean

@@ -297,9 +297,15 @@ lemma smul_mul_smul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
     (a • b) * (c • d) = (a * c) • (b * d) := by
   have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d
 
-@[to_additive (attr := deprecated (since := "2024-08-29"))]
+@[to_additive]
 alias smul_mul_smul := smul_mul_smul_comm
 
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated smul_mul_smul_comm (since := "2024-08-29")] smul_mul_smul
+attribute [deprecated vadd_add_vadd_comm (since := "2024-08-29")] vadd_add_vadd
+
+
 /-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
 satisfied by `Algebra α β`. -/
 @[to_additive]

Mathlib/Algebra/Group/AddChar.lean

@@ -253,7 +253,7 @@ lemma ne_one_iff : ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
 lemma ne_zero_iff : ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
 
 /-- An additive character is *nontrivial* if it takes a value `≠ 1`. -/
-@[deprecated (since := "2024-06-06")]
+@[deprecated "No deprecation message was provided." (since := "2024-06-06")]
 def IsNontrivial (ψ : AddChar A M) : Prop := ∃ a : A, ψ a ≠ 1
 
 set_option linter.deprecated false in

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -94,12 +94,28 @@ class MulEquivClass (F : Type*) (A B : outParam Type*) [Mul A] [Mul B] [EquivLik
   /-- Preserves multiplication. -/
   map_mul : ∀ (f : F) (a b), f (a * b) = f a * f b
 
-@[to_additive (attr := deprecated (since := "2024-11-10"))]
+@[to_additive]
 alias MulEquivClass.map_eq_one_iff := EmbeddingLike.map_eq_one_iff
 
-@[to_additive (attr := deprecated (since := "2024-11-10"))]
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated EmbeddingLike.map_eq_one_iff (since := "2024-11-10")]
+MulEquivClass.map_eq_one_iff
+attribute [deprecated EmbeddingLike.map_eq_zero_iff (since := "2024-11-10")]
+AddEquivClass.map_eq_zero_iff
+
+
+@[to_additive]
 alias MulEquivClass.map_ne_one_iff := EmbeddingLike.map_ne_one_iff
 
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated EmbeddingLike.map_ne_one_iff (since := "2024-11-10")]
+MulEquivClass.map_ne_one_iff
+attribute [deprecated EmbeddingLike.map_ne_zero_iff (since := "2024-11-10")]
+AddEquivClass.map_ne_zero_iff
+
+
 namespace MulEquivClass
 
 variable (F)

Mathlib/Algebra/Group/Pointwise/Set/Card.lean

@@ -33,7 +33,13 @@ lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
   refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_
   aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])
 
-@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_mul_le := natCard_mul_le
+@[to_additive] alias card_mul_le := natCard_mul_le
+
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated natCard_mul_le (since := "2024-09-30")] card_mul_le
+attribute [deprecated natCard_add_le (since := "2024-09-30")] card_add_le
+
 
 end Mul
 
@@ -48,7 +54,12 @@ lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by
 lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by
   rw [← image_inv, Nat.card_image_of_injective inv_injective]
 
-@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_inv := natCard_inv
+@[to_additive] alias card_inv := natCard_inv
+
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated natCard_inv (since := "2024-09-30")] card_inv
+attribute [deprecated natCard_neg (since := "2024-09-30")] card_neg
 
 @[to_additive (attr := simp)]
 lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by simp [encard, PartENat.card]
@@ -74,7 +85,12 @@ variable [Group G] {s t : Set G}
 lemma natCard_div_le : Nat.card (s / t) ≤ Nat.card s * Nat.card t := by
   rw [div_eq_mul_inv, ← natCard_inv t]; exact natCard_mul_le
 
-@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_div_le := natCard_div_le
+@[to_additive] alias card_div_le := natCard_div_le
+
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated natCard_div_le (since := "2024-09-30")] card_div_le
+attribute [deprecated natCard_sub_le (since := "2024-09-30")] card_sub_le
 
 variable [MulAction G α]
 
@@ -86,9 +102,14 @@ lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s :=
 lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s :=
   Nat.card_image_of_injective (MulAction.injective a) _
 
-@[to_additive (attr := deprecated (since := "2024-09-30"))]
+@[to_additive]
 alias card_smul_set := Cardinal.mk_smul_set
 
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated Cardinal.mk_smul_set (since := "2024-09-30")] card_smul_set
+attribute [deprecated Cardinal.mk_vadd_set (since := "2024-09-30")] card_vadd_set
+
 @[to_additive (attr := simp)]
 lemma encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard := by
   simp [encard, PartENat.card]

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -596,14 +596,14 @@ variable [Semiring R] [Module R M] [Semiring S] [Module S M₂] [Module R M₃]
 variable {σ : R →+* S}
 
 /-- A `DistribMulActionHom` between two modules is a linear map. -/
-@[deprecated (since := "2024-11-08")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
 def toSemilinearMap (fₗ : M →ₑ+[σ.toMonoidHom] M₂) : M →ₛₗ[σ] M₂ :=
   { fₗ with }
 
 instance : SemilinearMapClass (M →ₑ+[σ.toMonoidHom] M₂) σ M M₂ where
 
 /-- A `DistribMulActionHom` between two modules is a linear map. -/
-@[deprecated (since := "2024-11-08")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
 def toLinearMap (fₗ : M →+[R] M₃) : M →ₗ[R] M₃ :=
   { fₗ with }
 

Mathlib/Algebra/Order/Field/Power.lean

@@ -73,13 +73,13 @@ theorem zpow_injective (h₀ : 0 < a) (h₁ : a ≠ 1) : Injective (a ^ · : ℤ
 theorem zpow_inj (h₀ : 0 < a) (h₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
   zpow_right_inj₀ h₀ h₁
 
-@[deprecated (since := "2024-10-08")]
+@[deprecated "No deprecation message was provided." (since := "2024-10-08")]
 theorem zpow_le_max_of_min_le {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : min a b ≤ c) :
     x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) :=
   have : Antitone fun n : ℤ => x ^ (-n) := fun _ _ h => zpow_le_zpow_right₀ hx (neg_le_neg h)
   (this h).trans_eq this.map_min
 
-@[deprecated (since := "2024-10-08")]
+@[deprecated "No deprecation message was provided." (since := "2024-10-08")]
 theorem zpow_le_max_iff_min_le {x : α} (hx : 1 < x) {a b c : ℤ} :
     x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c := by
   simp_rw [le_max_iff, min_le_iff, zpow_le_zpow_iff_right₀ hx, neg_le_neg_iff]

Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

@@ -48,7 +48,12 @@ lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
 lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
   (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
 
-@[to_additive (attr := deprecated (since := "2024-11-13"))] alias Set.BddAbove.mul := BddAbove.mul
+@[to_additive] alias Set.BddAbove.mul := BddAbove.mul
+
+-- `alias` doesn't add the deprecation suggestion to the `to_additive` version
+-- see https://github.com/leanprover-community/mathlib4/issues/19424
+attribute [deprecated BddAbove.mul (since := "2024-11-13")] Set.BddAbove.mul
+attribute [deprecated BddAbove.add (since := "2024-11-13")] Set.BddAbove.add
 
 @[to_additive]
 lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) :

Mathlib/Analysis/Complex/Circle.lean

@@ -41,17 +41,17 @@ open ComplexConjugate
 /-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`.
 
 Please use `Circle` when referring to the circle as a type. -/
-@[deprecated (since := "2024-07-24")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-24")]
 def circle : Submonoid ℂ :=
   Submonoid.unitSphere ℂ
 
 set_option linter.deprecated false in
-@[deprecated (since := "2024-07-24")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-24")]
 theorem mem_circle_iff_abs {z : ℂ} : z ∈ circle ↔ abs z = 1 :=
   mem_sphere_zero_iff_norm
 
 set_option linter.deprecated false in
-@[deprecated (since := "2024-07-24")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-24")]
 theorem mem_circle_iff_normSq {z : ℂ} : z ∈ circle ↔ normSq z = 1 := by
   simp [Complex.abs, mem_circle_iff_abs]
 

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -92,7 +92,7 @@ lemma leftAdjoint_preservesColimits : PreservesColimitsOfSize.{v, u} F where
                 ((adj.functorialityAdjunction _).homEquiv _ _)⟩ } }
 
 include adj in
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma leftAdjointPreservesColimits : PreservesColimitsOfSize.{v, u} F :=
   adj.leftAdjoint_preservesColimits
 
@@ -117,7 +117,7 @@ noncomputable instance (priority := 100)
         { reflects := fun t =>
           ⟨(isColimitOfPreserves E.inv t).mapCoconeEquiv E.asEquivalence.unitIso.symm⟩ } }
 
-@[deprecated (since := "2024-11-18")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-18")]
 lemma isEquivalenceReflectsColimits (E : D ⥤ C) [E.IsEquivalence] :
     ReflectsColimitsOfSize.{v, u} E :=
   Functor.reflectsColimits_of_isEquivalence E
@@ -216,7 +216,7 @@ lemma rightAdjoint_preservesLimits : PreservesLimitsOfSize.{v, u} G where
                 ((adj.functorialityAdjunction' _).homEquiv _ _).symm⟩ } }
 
 include adj in
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma rightAdjointPreservesLimits : PreservesLimitsOfSize.{v, u} G :=
   adj.rightAdjoint_preservesLimits
 
@@ -240,7 +240,7 @@ noncomputable instance (priority := 100)
         { reflects := fun t =>
             ⟨(isLimitOfPreserves E.inv t).mapConeEquiv E.asEquivalence.unitIso.symm⟩ } }
 
-@[deprecated (since := "2024-11-18")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-18")]
 lemma isEquivalenceReflectsLimits (E : D ⥤ C) [E.IsEquivalence] :
     ReflectsLimitsOfSize.{v, u} E :=
   Functor.reflectsLimits_of_isEquivalence E

Mathlib/CategoryTheory/Idempotents/Karoubi.lean

@@ -111,7 +111,7 @@ theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f
 @[simp]
 theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl
 
-@[deprecated (since := "2024-07-15")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-15")]
 theorem id_eq {P : Karoubi C} : 𝟙 P = ⟨P.p, by repeat' rw [P.idem]⟩ := rfl
 
 /-- It is possible to coerce an object of `C` into an object of `Karoubi C`.

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -332,7 +332,7 @@ instance (priority := 100) preservesLimit_of_createsLimit_and_hasLimit (K : J 
     ((liftedLimitMapsToOriginal (limit.isLimit _)).symm ≪≫
       (Cones.functoriality K F).mapIso ((liftedLimitIsLimit (limit.isLimit _)).uniqueUpToIso t))⟩
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitOfCreatesLimitAndHasLimit (K : J ⥤ C) (F : C ⥤ D)
     [CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F :=
   preservesLimit_of_createsLimit_and_hasLimit _ _
@@ -342,7 +342,7 @@ lemma preservesLimitOfCreatesLimitAndHasLimit (K : J ⥤ C) (F : C ⥤ D)
 instance (priority := 100) preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
     (F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F where
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape
     (F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] :
     PreservesLimitsOfShape J F :=
@@ -354,7 +354,7 @@ instance (priority := 100) preservesLimits_of_createsLimits_and_hasLimits (F : C
     [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] :
     PreservesLimitsOfSize.{w, w'} F where
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitsOfCreatesLimitsAndHasLimits (F : C ⥤ D)
     [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] :
     PreservesLimitsOfSize.{w, w'} F :=
@@ -466,7 +466,7 @@ instance (priority := 100) preservesColimit_of_createsColimit_and_hasColimit (K
         (Cocones.functoriality K F).mapIso
           ((liftedColimitIsColimit (colimit.isColimit _)).uniqueUpToIso t))⟩
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesColimitOfCreatesColimitAndHasColimit (K : J ⥤ C) (F : C ⥤ D)
     [CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F :=
   preservesColimit_of_createsColimit_and_hasColimit _ _
@@ -477,7 +477,7 @@ instance (priority := 100) preservesColimitOfShape_of_createsColimitsOfShape_and
     (F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] :
     PreservesColimitsOfShape J F where
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape
     (F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] :
     PreservesColimitsOfShape J F :=
@@ -489,7 +489,7 @@ instance (priority := 100) preservesColimits_of_createsColimits_and_hasColimits
     [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] :
     PreservesColimitsOfSize.{w, w'} F where
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesColimitsOfCreatesColimitsAndHasColimits (F : C ⥤ D)
     [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] :
     PreservesColimitsOfSize.{w, w'} F :=

Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean

@@ -362,7 +362,7 @@ lemma preservesLimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)
     exact isLimitOfPreserves _ hc⟩⟩
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     (H : ∀ k : K, PreservesLimit G (F ⋙ (evaluation K C).obj k : D ⥤ C)) :
     PreservesLimit G F :=
@@ -374,7 +374,7 @@ lemma preservesLimitsOfShape_of_evaluation (F : D ⥤ K ⥤ C) (J : Type*) [Cate
     PreservesLimitsOfShape J F :=
   ⟨fun {G} => preservesLimit_of_evaluation F G fun _ => PreservesLimitsOfShape.preservesLimit⟩
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitsOfShapeOfEvaluation (F : D ⥤ K ⥤ C) (J : Type*) [Category J]
     (H : ∀ k : K, PreservesLimitsOfShape J (F ⋙ (evaluation K C).obj k)) :
     PreservesLimitsOfShape J F :=
@@ -387,7 +387,7 @@ lemma preservesLimits_of_evaluation (F : D ⥤ K ⥤ C)
   ⟨fun {L} _ =>
     preservesLimitsOfShape_of_evaluation F L fun _ => PreservesLimitsOfSize.preservesLimitsOfShape⟩
 
-@[deprecated (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided." (since := "2024-11-19")]
 lemma preservesLimitsOfEvaluation (F : D ⥤ K ⥤ C)
     (H : ∀ k : K, PreservesLimitsOfSize.{w', w} (F ⋙ (evaluation K C).obj k)) :
     PreservesLimitsOfSize.{w', w} F :=
@@ -412,7 +412,7 @@ lemma preservesColimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)
     exact isColimitOfPreserves _ hc⟩⟩
 
-@[deprecated  (since := "2024-11-19")]
+@[deprecated "No deprecation message was provided."  (since := "2024-11-19")]
 lemma preservesColimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     (H : ∀ k, PreservesColimit G (F ⋙ (evaluation K C).obj k)) : PreservesColimit G F :=
   preservesColimit_of_evaluation _ _ H

Mathlib/Data/Complex/Abs.lean

@@ -199,7 +199,7 @@ theorem abs_im_div_abs_le_one (z : ℂ) : |z.im / Complex.abs z| ≤ 1 :=
 
 @[simp, norm_cast] lemma abs_intCast (n : ℤ) : abs n = |↑n| := by rw [← ofReal_intCast, abs_ofReal]
 
-@[deprecated (since := "2024-02-14")]
+@[deprecated "No deprecation message was provided." (since := "2024-02-14")]
 lemma int_cast_abs (n : ℤ) : |↑n| = Complex.abs n := (abs_intCast _).symm
 
 theorem normSq_eq_abs (x : ℂ) : normSq x = (Complex.abs x) ^ 2 := by

Mathlib/Data/Fin/Basic.lean

@@ -1115,7 +1115,7 @@ lemma succAbove_ne_last {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last _)
 
 lemma succAbove_last_apply (i : Fin n) : succAbove (last n) i = castSucc i := by rw [succAbove_last]
 
-@[deprecated (since := "2024-05-30")]
+@[deprecated "No deprecation message was provided." (since := "2024-05-30")]
 lemma succAbove_lt_ge (p : Fin (n + 1)) (i : Fin n) :
     castSucc i < p ∨ p ≤ castSucc i := Nat.lt_or_ge (castSucc i) p
 

Mathlib/Data/List/Basic.lean

@@ -34,7 +34,7 @@ universe u v w
 variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {l₁ l₂ : List α}
 
 /-- `≤` implies not `>` for lists. -/
-@[deprecated (since := "2024-07-27")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-27")]
 theorem le_eq_not_gt [LT α] : ∀ l₁ l₂ : List α, (l₁ ≤ l₂) = ¬l₂ < l₁ := fun _ _ => rfl
 
 -- Porting note: Delete this attribute
@@ -496,7 +496,7 @@ theorem get_tail (l : List α) (i) (h : i < l.tail.length)
     l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩ := by
   cases l <;> [cases h; rfl]
 
-@[deprecated (since := "2024-08-22")]
+@[deprecated "No deprecation message was provided." (since := "2024-08-22")]
 theorem get_cons {l : List α} {a : α} {n} (hl) :
     (a :: l).get ⟨n, hl⟩ = if hn : n = 0 then a else
       l.get ⟨n - 1, by contrapose! hl; rw [length_cons]; omega⟩ :=
@@ -627,7 +627,7 @@ lemma cons_sublist_cons' {a b : α} : a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l
 
 theorem sublist_cons_of_sublist (a : α) (h : l₁ <+ l₂) : l₁ <+ a :: l₂ := h.cons _
 
-@[deprecated (since := "2024-04-07")]
+@[deprecated "No deprecation message was provided." (since := "2024-04-07")]
 theorem sublist_of_cons_sublist_cons {a} (h : a :: l₁ <+ a :: l₂) : l₁ <+ l₂ := h.of_cons_cons
 
 @[deprecated (since := "2024-04-07")] alias cons_sublist_cons_iff := cons_sublist_cons
@@ -2281,7 +2281,7 @@ theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs
   simp; omega
 
 set_option linter.deprecated false in
-@[deprecated (since := "2024-07-25")]
+@[deprecated "No deprecation message was provided." (since := "2024-07-25")]
 theorem sizeOf_dropSlice_lt [SizeOf α] (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
     SizeOf.sizeOf (List.dropSlice i j xs) < SizeOf.sizeOf xs := by
   induction xs generalizing i j hj with

Mathlib/Data/List/Flatten.lean

@@ -158,7 +158,8 @@ theorem append_flatten_map_append (L : List (List α)) (x : List α) :
 
 @[deprecated (since := "2024-10-15")] alias append_join_map_append := append_flatten_map_append
 
-@[deprecated (since := "2024-08-15")] theorem sublist_join {l} {L : List (List α)} (h : l ∈ L) :
+@[deprecated "No deprecation message was provided." (since := "2024-08-15")]
+theorem sublist_join {l} {L : List (List α)} (h : l ∈ L) :
     l <+ L.flatten :=
   sublist_flatten_of_mem h