chore: reformat deprecation warnings on one line, if possible (#12335)

Occasionally, remove a "deprecated by" or "deprecated since", to fit the line length.

This is desirable (to me) because
- it's more compact: 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/Order/Field/Power.lean

@@ -83,8 +83,7 @@ theorem zpow_lt_iff_lt (hx : 1 < a) : a ^ m < a ^ n ↔ m < n :=
 
 @[gcongr] alias ⟨_, GCongr.zpow_lt_of_lt⟩ := zpow_lt_iff_lt
 
-@[deprecated] -- Since 2024-02-10
-alias zpow_lt_of_lt := GCongr.zpow_lt_of_lt
+@[deprecated] alias zpow_lt_of_lt := GCongr.zpow_lt_of_lt -- Since 2024-02-10
 
 @[simp]
 theorem zpow_le_iff_le (hx : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -288,8 +288,7 @@ lemma pow_lt_pow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by
   induction' hmn with n _ ih; exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)]
 #align pow_lt_pow₀ pow_lt_pow_right₀
 
--- 2023-12-23
-@[deprecated] alias pow_lt_pow₀ := pow_lt_pow_right₀
+@[deprecated] alias pow_lt_pow₀ := pow_lt_pow_right₀ -- 2023-12-23
 
 end LinearOrderedCommGroupWithZero
 

Mathlib/Algebra/Squarefree/Basic.lean

@@ -320,7 +320,6 @@ theorem squarefree_natCast {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n :=
   rw [← squarefree_natAbs, natAbs_ofNat]
 #align int.squarefree_coe_nat Int.squarefree_natCast
 
--- 2024-04-05
-@[deprecated] alias squarefree_coe_nat := squarefree_natCast
+@[deprecated] alias squarefree_coe_nat := squarefree_natCast -- 2024-04-05
 
 end Int

Mathlib/Analysis/Convex/Integral.lean

@@ -364,6 +364,6 @@ theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const [StrictConvexSpace 
   exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le
 #align ae_eq_const_or_norm_set_integral_lt_of_norm_le_const ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const
 
-@[deprecated]
+@[deprecated] -- 2024-04-17
 alias ae_eq_const_or_norm_set_integral_lt_of_norm_le_const :=
-  ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const -- deprecated on 2024-04-17
+  ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const

Mathlib/Analysis/Matrix.lean

@@ -272,54 +272,42 @@ theorem linfty_opNorm_def (A : Matrix m n α) :
   simp [Pi.norm_def, PiLp.nnnorm_eq_sum ENNReal.one_ne_top]
 #align matrix.linfty_op_norm_def Matrix.linfty_opNorm_def
 
-@[deprecated]
-alias linfty_op_norm_def :=
-  linfty_opNorm_def -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_def := linfty_opNorm_def -- 2024-02-02
 
 theorem linfty_opNNNorm_def (A : Matrix m n α) :
     ‖A‖₊ = (Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ :=
   Subtype.ext <| linfty_opNorm_def A
 #align matrix.linfty_op_nnnorm_def Matrix.linfty_opNNNorm_def
 
-@[deprecated]
-alias linfty_op_nnnorm_def :=
-  linfty_opNNNorm_def -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_def := linfty_opNNNorm_def -- 2024-02-02
 
 @[simp, nolint simpNF] -- Porting note: linter times out
 theorem linfty_opNNNorm_col (v : m → α) : ‖col v‖₊ = ‖v‖₊ := by
   rw [linfty_opNNNorm_def, Pi.nnnorm_def]
   simp
 #align matrix.linfty_op_nnnorm_col Matrix.linfty_opNNNorm_col
 
-@[deprecated]
-alias linfty_op_nnnorm_col :=
-  linfty_opNNNorm_col -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_col := linfty_opNNNorm_col -- 2024-02-02
 
 @[simp]
 theorem linfty_opNorm_col (v : m → α) : ‖col v‖ = ‖v‖ :=
   congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_col v
 #align matrix.linfty_op_norm_col Matrix.linfty_opNorm_col
 
-@[deprecated]
-alias linfty_op_norm_col :=
-  linfty_opNorm_col -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_col := linfty_opNorm_col -- 2024-02-02
 
 @[simp]
 theorem linfty_opNNNorm_row (v : n → α) : ‖row v‖₊ = ∑ i, ‖v i‖₊ := by simp [linfty_opNNNorm_def]
 #align matrix.linfty_op_nnnorm_row Matrix.linfty_opNNNorm_row
 
-@[deprecated]
-alias linfty_op_nnnorm_row :=
-  linfty_opNNNorm_row -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_row := linfty_opNNNorm_row -- 2024-02-02
 
 @[simp]
 theorem linfty_opNorm_row (v : n → α) : ‖row v‖ = ∑ i, ‖v i‖ :=
   (congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_row v).trans <| by simp [NNReal.coe_sum]
 #align matrix.linfty_op_norm_row Matrix.linfty_opNorm_row
 
-@[deprecated]
-alias linfty_op_norm_row :=
-  linfty_opNorm_row -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_row := linfty_opNorm_row -- deprecated on 2024-02-02
 
 @[simp]
 theorem linfty_opNNNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v‖₊ = ‖v‖₊ := by
@@ -330,18 +318,14 @@ theorem linfty_opNNNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v
   · rw [diagonal_apply_eq]
 #align matrix.linfty_op_nnnorm_diagonal Matrix.linfty_opNNNorm_diagonal
 
-@[deprecated]
-alias linfty_op_nnnorm_diagonal :=
-  linfty_opNNNorm_diagonal -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_diagonal := linfty_opNNNorm_diagonal -- 2024-02-02
 
 @[simp]
 theorem linfty_opNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v‖ = ‖v‖ :=
   congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_diagonal v
 #align matrix.linfty_op_norm_diagonal Matrix.linfty_opNorm_diagonal
 
-@[deprecated]
-alias linfty_op_norm_diagonal :=
-  linfty_opNorm_diagonal -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_diagonal := linfty_opNorm_diagonal -- deprecated on 2024-02-02
 
 end SeminormedAddCommGroup
 
@@ -368,34 +352,26 @@ theorem linfty_opNNNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B
       rfl
 #align matrix.linfty_op_nnnorm_mul Matrix.linfty_opNNNorm_mul
 
-@[deprecated]
-alias linfty_op_nnnorm_mul :=
-  linfty_opNNNorm_mul -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_mul := linfty_opNNNorm_mul -- deprecated on 2024-02-02
 
 theorem linfty_opNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖ ≤ ‖A‖ * ‖B‖ :=
   linfty_opNNNorm_mul _ _
 #align matrix.linfty_op_norm_mul Matrix.linfty_opNorm_mul
 
-@[deprecated]
-alias linfty_op_norm_mul :=
-  linfty_opNorm_mul -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_mul := linfty_opNorm_mul -- deprecated on 2024-02-02
 
 theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊ := by
   rw [← linfty_opNNNorm_col (A *ᵥ v), ← linfty_opNNNorm_col v]
   exact linfty_opNNNorm_mul A (col v)
 #align matrix.linfty_op_nnnorm_mul_vec Matrix.linfty_opNNNorm_mulVec
 
-@[deprecated]
-alias linfty_op_nnnorm_mulVec :=
-  linfty_opNNNorm_mulVec -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_mulVec := linfty_opNNNorm_mulVec -- deprecated on 2024-02-02
 
 theorem linfty_opNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ :=
   linfty_opNNNorm_mulVec _ _
 #align matrix.linfty_op_norm_mul_vec Matrix.linfty_opNorm_mulVec
 
-@[deprecated]
-alias linfty_op_norm_mulVec :=
-  linfty_opNorm_mulVec -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_mulVec := linfty_opNorm_mulVec -- deprecated on 2024-02-02
 
 end NonUnitalSeminormedRing
 
@@ -501,17 +477,13 @@ lemma linfty_opNNNorm_eq_opNNNorm (A : Matrix m n α) :
     nnnorm_one, mul_one] at hN
   exact hN
 
-@[deprecated]
-alias linfty_op_nnnorm_eq_op_nnnorm :=
-  linfty_opNNNorm_eq_opNNNorm -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_eq_op_nnnorm := linfty_opNNNorm_eq_opNNNorm -- 2024-02-02
 
 lemma linfty_opNorm_eq_opNorm (A : Matrix m n α) :
     ‖A‖ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖ :=
   congr_arg NNReal.toReal (linfty_opNNNorm_eq_opNNNorm A)
 
-@[deprecated]
-alias linfty_op_norm_eq_op_norm :=
-  linfty_opNorm_eq_opNorm -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_eq_op_norm := linfty_opNorm_eq_opNorm -- 2024-02-02
 
 variable [DecidableEq n]
 
@@ -520,17 +492,13 @@ variable [DecidableEq n]
   rw [linfty_opNNNorm_eq_opNNNorm]
   simp only [← toLin'_apply', toLin'_toMatrix']
 
-@[deprecated]
-alias linfty_op_nnnorm_toMatrix :=
-  linfty_opNNNorm_toMatrix -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_nnnorm_toMatrix := linfty_opNNNorm_toMatrix -- 2024-02-02
 
 @[simp] lemma linfty_opNorm_toMatrix (f : (n → α) →L[α] (m → α)) :
     ‖LinearMap.toMatrix' (↑f : (n → α) →ₗ[α] (m → α))‖ = ‖f‖ :=
   congr_arg NNReal.toReal (linfty_opNNNorm_toMatrix f)
 
-@[deprecated]
-alias linfty_op_norm_toMatrix :=
-  linfty_opNorm_toMatrix -- deprecated on 2024-02-02
+@[deprecated] alias linfty_op_norm_toMatrix := linfty_opNorm_toMatrix -- 2024-02-02
 
 end
 

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1929,8 +1929,7 @@ theorem norm_eq_abs (n : ℤ) : ‖n‖ = |(n : ℝ)| :=
 theorem norm_natCast (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs]
 #align int.norm_coe_nat Int.norm_natCast
 
--- 2024-04-05
-@[deprecated] alias norm_coe_nat := norm_natCast
+@[deprecated] alias norm_coe_nat := norm_natCast -- 2024-04-05
 
 theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
   NNReal.eq <|

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -312,19 +312,15 @@ theorem Basis.opNNNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E
       _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
 #align basis.op_nnnorm_le Basis.opNNNorm_le
 
-@[deprecated]
-alias Basis.op_nnnorm_le :=
-  Basis.opNNNorm_le -- deprecated on 2024-02-02
+@[deprecated] alias Basis.op_nnnorm_le := Basis.opNNNorm_le -- deprecated on 2024-02-02
 
 theorem Basis.opNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ}
     (hM : 0 ≤ M) (hu : ∀ i, ‖u (v i)‖ ≤ M) :
     ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M := by
   simpa using NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)
 #align basis.op_norm_le Basis.opNorm_le
 
-@[deprecated]
-alias Basis.op_norm_le :=
-  Basis.opNorm_le -- deprecated on 2024-02-02
+@[deprecated] alias Basis.op_norm_le := Basis.opNorm_le -- deprecated on 2024-02-02
 
 /-- A weaker version of `Basis.opNNNorm_le` that abstracts away the value of `C`. -/
 theorem Basis.exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
@@ -336,9 +332,7 @@ theorem Basis.exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E)
       (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩
 #align basis.exists_op_nnnorm_le Basis.exists_opNNNorm_le
 
-@[deprecated]
-alias Basis.exists_op_nnnorm_le :=
-  Basis.exists_opNNNorm_le -- deprecated on 2024-02-02
+@[deprecated] alias Basis.exists_op_nnnorm_le := Basis.exists_opNNNorm_le -- 2024-02-02
 
 /-- A weaker version of `Basis.opNorm_le` that abstracts away the value of `C`. -/
 theorem Basis.exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
@@ -350,9 +344,7 @@ theorem Basis.exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
   simpa using h ⟨M, hM⟩ H
 #align basis.exists_op_norm_le Basis.exists_opNorm_le
 
-@[deprecated]
-alias Basis.exists_op_norm_le :=
-  Basis.exists_opNorm_le -- deprecated on 2024-02-02
+@[deprecated] alias Basis.exists_op_norm_le := Basis.exists_opNorm_le -- deprecated on 2024-02-02
 
 instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] :
     SecondCountableTopology (E →L[𝕜] F) := by

Mathlib/Analysis/NormedSpace/Int.lean

@@ -35,8 +35,7 @@ theorem nnnorm_natCast (n : ℕ) : ‖(n : ℤ)‖₊ = n :=
   Real.nnnorm_natCast _
 #align int.nnnorm_coe_nat Int.nnnorm_natCast
 
--- 2024-04-05
-@[deprecated] alias nnnorm_coe_nat := nnnorm_natCast
+@[deprecated] alias nnnorm_coe_nat := nnnorm_natCast -- 2024-04-05
 
 @[simp]
 theorem toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊ := by