chore: unify date formatting in lemma deprecations (#12334)

- consistently use the YYYY-MM-DD format
- when easily possible, put the date on the same line as the `deprecated` attribute
- when easily possible, format the entire declaration on the same line

Why these changes?
- consistency makes it easier for tools to parse this information
- compactness: I don't see a good reason for these declarations taking up more space than needed;
 as I understand it, deprecated lemmas are not supposed to be used in mathlib anyway
- putting the date on the same line as the attribute makes it easier to discover un-dated deprecations;
they also ease writing a tool to replace these by a machine-readable version using leanprover/lean4#3968

Mathlib/Algebra/Associated.lean

@@ -1026,7 +1026,7 @@ theorem isPrimal_mk {a : α} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by
     exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
   · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩
 
-@[deprecated] alias isPrimal_iff := isPrimal_mk -- 2024/03/16
+@[deprecated] alias isPrimal_iff := isPrimal_mk -- 2024-03-16
 
 @[simp]
 theorem decompositionMonoid_iff : DecompositionMonoid (Associates α) ↔ DecompositionMonoid α := by

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2499,11 +2499,5 @@ theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative α) :
 
 end AddCommMonoid
 
-/-!
-### Deprecated lemmas
-
-Those lemmas were deprecated on the 2023/12/23.
--/
-
-@[deprecated] alias Equiv.prod_comp' := Fintype.prod_equiv
-@[deprecated] alias Equiv.sum_comp' := Fintype.sum_equiv
+@[deprecated] alias Equiv.prod_comp' := Fintype.prod_equiv -- 2023-12-23
+@[deprecated] alias Equiv.sum_comp' := Fintype.sum_equiv -- 2023-12-23

Mathlib/Algebra/Group/Units.lean

@@ -1214,7 +1214,7 @@ noncomputable def commGroupOfIsUnit [hM : CommMonoid M] (h : ∀ a : M, IsUnit a
 
 end NoncomputableDefs
 
--- 2024--03-20
+-- 2024-03-20
 attribute [deprecated div_mul_cancel_right] IsUnit.div_mul_left
 attribute [deprecated sub_add_cancel_right] IsAddUnit.sub_add_left
 attribute [deprecated div_mul_cancel_left] IsUnit.div_mul_right

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -125,8 +125,8 @@ lemma trace_comp_toEndomorphism_weightSpace_eq (χ : L → R) :
   rw [LinearMap.comp_apply, LieHom.coe_toLinearMap, h₁, map_add, h₂]
   simp [mul_comm (χ x)]
 
-@[deprecated] alias trace_comp_toEndomorphism_weight_space_eq :=
-  trace_comp_toEndomorphism_weightSpace_eq -- 2024-04-06
+@[deprecated] -- 2024-04-06
+alias trace_comp_toEndomorphism_weight_space_eq := trace_comp_toEndomorphism_weightSpace_eq
 
 variable {R L M} in
 lemma zero_lt_finrank_weightSpace {χ : L → R} (hχ : weightSpace M χ ≠ ⊥) :

Mathlib/Algebra/Module/Basic.lean

@@ -105,7 +105,8 @@ theorem two_smul : (2 : R) • x = x + x := by rw [← one_add_one_eq_two, add_s
 #align two_smul two_smul
 
 set_option linter.deprecated false in
-@[deprecated] theorem two_smul' : (2 : R) • x = bit0 x :=
+@[deprecated]
+theorem two_smul' : (2 : R) • x = bit0 x :=
   two_smul R x
 #align two_smul' two_smul'
 

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -191,8 +191,7 @@ lemma IsAbsoluteValue.abv_sum [Semiring R] [OrderedSemiring S] (abv : R → S) [
   (IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _
 #align is_absolute_value.abv_sum IsAbsoluteValue.abv_sum
 
---  2024-02-14
-@[deprecated] alias abv_sum_le_sum_abv := IsAbsoluteValue.abv_sum
+@[deprecated] alias abv_sum_le_sum_abv := IsAbsoluteValue.abv_sum -- 2024-02-14
 
 nonrec lemma AbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S]
     (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) :

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -1325,12 +1325,7 @@ instance (priority := 100) LinearOrderedCommRing.toLinearOrderedCommSemiring
   { d, LinearOrderedRing.toLinearOrderedSemiring with }
 #align linear_ordered_comm_ring.to_linear_ordered_comm_semiring LinearOrderedCommRing.toLinearOrderedCommSemiring
 
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on 2023/12/23
--/
-
+-- 2023-12-23
 @[deprecated] alias zero_le_mul_left := mul_nonneg_iff_of_pos_left
 @[deprecated] alias zero_le_mul_right := mul_nonneg_iff_of_pos_right
 @[deprecated] alias zero_lt_mul_left := mul_pos_iff_of_pos_left

Mathlib/Algebra/Polynomial/Div.lean

@@ -412,8 +412,7 @@ theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p :=
     exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.some_lt_some.1 this)⟩
 #align polynomial.dvd_iff_mod_by_monic_eq_zero Polynomial.modByMonic_eq_zero_iff_dvd
 
--- 2024-03-23
-@[deprecated] alias dvd_iff_modByMonic_eq_zero := modByMonic_eq_zero_iff_dvd
+@[deprecated] alias dvd_iff_modByMonic_eq_zero := modByMonic_eq_zero_iff_dvd -- 2024-03-23
 
 /-- See `Polynomial.mul_left_modByMonic` for the other multiplication order. That version, unlike
 this one, requires commutativity. -/

Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean

@@ -217,5 +217,5 @@ theorem isOpenMap_of_hasStrictFDerivAt_equiv [CompleteSpace E] {f : E → F} {f'
     (hf : ∀ x, HasStrictFDerivAt f (f' x : E →L[𝕜] F) x) : IsOpenMap f :=
   isOpenMap_iff_nhds_le.2 fun x => (hf x).map_nhds_eq_of_equiv.ge
 #align open_map_of_strict_fderiv_equiv isOpenMap_of_hasStrictFDerivAt_equiv
-@[deprecated] alias open_map_of_strict_fderiv_equiv :=
-  isOpenMap_of_hasStrictFDerivAt_equiv -- 2024-03-23
+@[deprecated] -- 2024-03-23
+alias open_map_of_strict_fderiv_equiv := isOpenMap_of_hasStrictFDerivAt_equiv

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -147,8 +147,8 @@ theorem fourierIntegral_convergent_iff (he : Continuous e)
   exact this
 #align vector_fourier.fourier_integral_convergent_iff VectorFourier.fourierIntegral_convergent_iff
 
-@[deprecated] alias fourier_integral_convergent_iff :=
-  VectorFourier.fourierIntegral_convergent_iff -- 2024-03-29
+@[deprecated] -- 2024-03-29
+alias fourier_integral_convergent_iff := VectorFourier.fourierIntegral_convergent_iff
 
 variable [CompleteSpace E]
 
@@ -463,8 +463,8 @@ theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
     mul_assoc]
 #align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_real_eq_integral_exp_smul
 
-@[deprecated] alias fourierIntegral_eq_integral_exp_smul :=
-  fourierIntegral_real_eq_integral_exp_smul -- deprecated on 2024-02-21
+@[deprecated] -- deprecated on 2024-02-21
+alias fourierIntegral_eq_integral_exp_smul := fourierIntegral_real_eq_integral_exp_smul
 
 @[simp] theorem fourierIntegral_convergent_iff {μ : Measure V} {f : V → E} (w : V) :
     Integrable (fun v : V ↦ 𝐞 (- ⟪v, w⟫) • f v) μ ↔ Integrable f μ :=

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

@@ -80,7 +80,7 @@ lemma FiniteDimensional.of_fact_finrank_eq_two {K V : Type*} [DivisionRing K]
 
 attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 
-@[deprecated] -- Since 2024/02/02
+@[deprecated] -- Since 2024-02-02
 alias FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two :=
   FiniteDimensional.of_fact_finrank_eq_two
 

Mathlib/Analysis/LocallyConvex/Basic.lean

@@ -236,8 +236,7 @@ theorem Balanced.smul_mem_iff (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a
   ⟨(hs.smul_mem_mono · h.ge), (hs.smul_mem_mono · h.le)⟩
 #align balanced.mem_smul_iff Balanced.smul_mem_iff
 
-@[deprecated] -- Since 2024/02/02
-alias Balanced.mem_smul_iff := Balanced.smul_mem_iff
+@[deprecated] alias Balanced.mem_smul_iff := Balanced.smul_mem_iff -- since 2024-02-02
 
 variable [TopologicalSpace E] [ContinuousSMul 𝕜 E]
 
@@ -281,7 +280,7 @@ section NontriviallyNormedField
 
 variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E}
 
-@[deprecated Absorbent.zero_mem] -- Since 2024/02/02
+@[deprecated Absorbent.zero_mem] -- Since 2024-02-02
 theorem Absorbent.zero_mem' (hs : Absorbent 𝕜 s) : (0 : E) ∈ s := hs.zero_mem
 
 variable [Module ℝ E] [SMulCommClass ℝ 𝕜 E]
@@ -296,8 +295,7 @@ protected theorem Balanced.convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (co
   exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv
 #align balanced_convex_hull_of_balanced Balanced.convexHull
 
-@[deprecated] -- Since 2024/02/02
-alias balanced_convexHull_of_balanced := Balanced.convexHull
+@[deprecated] alias balanced_convexHull_of_balanced := Balanced.convexHull -- Since 2024-02-02
 
 end NontriviallyNormedField
 

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -84,7 +84,7 @@ theorem _root_.Filter.HasBasis.isVonNBounded_iff {q : ι → Prop} {s : ι → S
   exact (hA i hi).mono_left hV
 #align filter.has_basis.is_vonN_bounded_basis_iff Filter.HasBasis.isVonNBounded_iff
 
-@[deprecated] -- since 12 January 2024
+@[deprecated] -- since 2024-01-12
 alias _root_.Filter.HasBasis.isVonNBounded_basis_iff := Filter.HasBasis.isVonNBounded_iff
 
 /-- Subsets of bounded sets are bounded. -/

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -493,7 +493,7 @@ theorem FiniteDimensional.of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
     _ < ‖c‖ := hN (N + 1) (Nat.le_succ N)
 #align finite_dimensional_of_is_compact_closed_ball₀ FiniteDimensional.of_isCompact_closedBall₀
 
-@[deprecated] -- Since 2024/02/02
+@[deprecated] -- Since 2024-02-02
 alias finiteDimensional_of_isCompact_closedBall₀ := FiniteDimensional.of_isCompact_closedBall₀
 
 /-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
@@ -503,7 +503,7 @@ theorem FiniteDimensional.of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c :
   .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)
 #align finite_dimensional_of_is_compact_closed_ball FiniteDimensional.of_isCompact_closedBall
 
-@[deprecated] -- Since 2024/02/02
+@[deprecated] -- Since 2024-02-02
 alias finiteDimensional_of_isCompact_closedBall := FiniteDimensional.of_isCompact_closedBall
 
 /-- **Riesz's theorem**: a locally compact normed vector space is finite-dimensional. -/
@@ -512,7 +512,7 @@ theorem FiniteDimensional.of_locallyCompactSpace [LocallyCompactSpace E] :
   let ⟨_r, rpos, hr⟩ := exists_isCompact_closedBall (0 : E)
   .of_isCompact_closedBall₀ 𝕜 rpos hr
 
-@[deprecated] -- Since 2024/02/02
+@[deprecated] -- Since 2024-02-02
 alias finiteDimensional_of_locallyCompactSpace := FiniteDimensional.of_locallyCompactSpace
 
 /-- If a function has compact support, then either the function is trivial
@@ -548,7 +548,7 @@ lemma ProperSpace.of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField
     Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
   exact .of_seq_closedBall hTop (eventually_of_forall hC)
 
-@[deprecated] -- Since 2024/01/31
+@[deprecated] -- Since 2024-01-31
 alias properSpace_of_locallyCompactSpace := ProperSpace.of_locallyCompactSpace
 
 variable (E)
@@ -561,7 +561,7 @@ lemma ProperSpace.of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E
     apply ClosedEmbedding.locallyCompactSpace this
   .of_locallyCompactSpace 𝕜
 
-@[deprecated] -- Since 2024/01/31
+@[deprecated] -- Since 2024-01-31
 alias properSpace_of_locallyCompact_module := ProperSpace.of_locallyCompact_module
 
 end Riesz

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -1379,9 +1379,7 @@ theorem opNorm_zero_iff : ‖f‖ = 0 ↔ f = 0 := by
   simp [← (opNorm_nonneg f).le_iff_eq, opNorm_le_iff f le_rfl, ext_iff]
 #align continuous_multilinear_map.op_norm_zero_iff ContinuousMultilinearMap.opNorm_zero_iff
 
-@[deprecated]
-alias op_norm_zero_iff :=
-  opNorm_zero_iff -- deprecated on 2024-02-02
+@[deprecated] alias op_norm_zero_iff := opNorm_zero_iff -- deprecated on 2024-02-02
 
 /-- Continuous multilinear maps themselves form a normed group with respect to
     the operator norm. -/

Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

@@ -223,8 +223,7 @@ theorem _root_.fourierIntegral_gaussian (hb : 0 < b.re) (t : ℂ) :
     mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]
 #align fourier_transform_gaussian fourierIntegral_gaussian
 
-@[deprecated] alias _root_.fourier_transform_gaussian :=
-  fourierIntegral_gaussian -- deprecated on 2024-02-21
+@[deprecated] alias _root_.fourier_transform_gaussian := fourierIntegral_gaussian -- 2024-02-21
 
 theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
     (𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ =>
@@ -246,17 +245,17 @@ theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
     simp only [I_sq]
     ring
 
-@[deprecated] alias _root_.fourier_transform_gaussian_pi' :=
-  _root_.fourierIntegral_gaussian_pi' -- deprecated on 2024-02-21
+@[deprecated] -- deprecated on 2024-02-21
+alias _root_.fourier_transform_gaussian_pi' := _root_.fourierIntegral_gaussian_pi'
 
 theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) :
     (𝓕 fun (x : ℝ) ↦ cexp (-π * b * x ^ 2)) =
     fun t : ℝ ↦ 1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * t ^ 2) := by
   simpa only [mul_zero, zero_mul, add_zero] using fourierIntegral_gaussian_pi' hb 0
 #align fourier_transform_gaussian_pi fourierIntegral_gaussian_pi
 
-@[deprecated] alias root_.fourier_transform_gaussian_pi :=
-  _root_.fourierIntegral_gaussian_pi   -- deprecated on 2024-02-21
+@[deprecated] -- 2024-02-21
+alias root_.fourier_transform_gaussian_pi := _root_.fourierIntegral_gaussian_pi
 
 section InnerProductSpace
 

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -1051,10 +1051,4 @@ end Mathlib.Meta.NormNum
 
 end Tactics
 
-/-!
-### Deprecated lemmas
-
-These lemmas have been deprecated on 2024-01-07.
--/
-
-@[deprecated] alias rpow_nonneg_of_nonneg := rpow_nonneg
+@[deprecated] alias rpow_nonneg_of_nonneg := rpow_nonneg -- 2024-01-07

Mathlib/Data/Complex/Abs.lean

@@ -243,8 +243,8 @@ 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]
 #align complex.int_cast_abs Complex.abs_intCast
 
--- 2024-02-14
-@[deprecated] lemma int_cast_abs (n : ℤ) : |↑n| = Complex.abs n := (abs_intCast _).symm
+@[deprecated] -- 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
   simp [abs, sq, abs_def, Real.mul_self_sqrt (normSq_nonneg _)]

Mathlib/Data/ENNReal/Basic.lean

@@ -870,11 +870,6 @@ def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do
 
 end Mathlib.Meta.Positivity
 
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on the 2023/12/23.
--/
-
+-- 2023-12-23
 @[deprecated] protected alias ENNReal.le_inv_smul_iff_of_pos := le_inv_smul_iff_of_pos
 @[deprecated] protected alias ENNReal.inv_smul_le_iff_of_pos := inv_smul_le_iff_of_pos

Mathlib/Data/Finset/Card.lean

@@ -849,12 +849,6 @@ theorem lt_wf {α} : WellFounded (@LT.lt (Finset α) _) :=
   Subrelation.wf H <| InvImage.wf _ <| (Nat.lt_wfRel).2
 #align finset.lt_wf Finset.lt_wf
 
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on 2023-12-27.
--/
-
-@[deprecated] alias card_le_of_subset := card_le_card
+@[deprecated] alias card_le_of_subset := card_le_card -- 2023-12-27
 
 end Finset

Mathlib/Data/Finset/Image.lean

@@ -435,7 +435,7 @@ protected theorem Nonempty.image (h : s.Nonempty) (f : α → β) : (s.image f).
 
 alias ⟨Nonempty.of_image, _⟩ := image_nonempty
 
-@[deprecated image_nonempty] -- Since 29 December 2023
+@[deprecated image_nonempty] -- 2023-12-29
 theorem Nonempty.image_iff (f : α → β) : (s.image f).Nonempty ↔ s.Nonempty :=
   image_nonempty
 
@@ -901,14 +901,8 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
 
 end Equiv
 
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on 2023-12-27.
--/
-
 namespace Finset
 
-@[deprecated] alias image_filter := filter_image
+@[deprecated] alias image_filter := filter_image -- 2023-12-27
 
 end Finset

Mathlib/Data/Int/Defs.lean

@@ -63,8 +63,8 @@ instance instNontrivial : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩
 
 @[simp] lemma ofNat_eq_natCast : Int.ofNat n = n := rfl
 
--- 2024-03-24
-@[deprecated ofNat_eq_natCast] protected lemma natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n := rfl
+@[deprecated ofNat_eq_natCast] -- 2024-03-24
+protected lemma natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n := rfl
 #align int.coe_nat_eq Int.natCast_eq_ofNat
 
 @[norm_cast] lemma natCast_inj : (m : ℤ) = (n : ℤ) ↔ m = n := ofNat_inj

Mathlib/Data/Int/ModEq.lean

@@ -325,7 +325,6 @@ theorem mod_mul_left_mod (a b c : ℤ) : a % (b * c) % c = a % c :=
   (mod_modEq _ _).of_mul_left _
 #align int.mod_mul_left_mod Int.mod_mul_left_mod
 
--- 2024-04-02
-@[deprecated] alias coe_nat_modEq_iff := natCast_modEq_iff
+@[deprecated] alias coe_nat_modEq_iff := natCast_modEq_iff -- 2024-04-02
 
 end Int

Mathlib/Data/Multiset/Basic.lean

@@ -3208,13 +3208,7 @@ theorem coe_subsingletonEquiv [Subsingleton α] :
   rfl
 #align multiset.coe_subsingleton_equiv Multiset.coe_subsingletonEquiv
 
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on 2023-12-27.
--/
-
-@[deprecated] alias card_le_of_le := card_le_card
-@[deprecated] alias card_lt_of_lt := card_lt_card
+@[deprecated] alias card_le_of_le := card_le_card -- 2023-12-27
+@[deprecated] alias card_lt_of_lt := card_lt_card -- 2023-12-27
 
 end Multiset

Mathlib/Data/NNRat/Defs.lean

@@ -195,8 +195,7 @@ theorem mk_natCast (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ
   rfl
 #align nnrat.mk_coe_nat NNRat.mk_natCast
 
--- 2024-04-05
-@[deprecated] alias mk_coe_nat := mk_natCast
+@[deprecated] alias mk_coe_nat := mk_natCast -- 2024-04-05
 
 @[simp]
 theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) :=