From d334e96275e49598fbd4c0cb93d66ef13fb0cab6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 17 Jun 2024 09:46:44 +0100
Subject: [PATCH] chore: add forgotten deprecation (#4475)

---
 src/Init/Data/List/Lemmas.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index f19b861d3c..83ebec58af 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -61,6 +61,8 @@ theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (c
 theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
   ⟨tail_eq_of_cons_eq, congrArg _⟩
 
+@[deprecated (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right
+
 theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
   List.cons.injEq .. ▸ .rfl