From 5f963d5d06cc3c2d3abd0806891133137a59d7eb Mon Sep 17 00:00:00 2001
From: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Mon, 14 Oct 2024 07:38:45 +0000
Subject: [PATCH] chore: remove duplicate theorem about lists (#986)

---
 Batteries/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 96a79c5bfa..6a956f9b1d 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -17,7 +17,7 @@ namespace List
 
 /-! ### isEmpty -/
 
-theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
+@[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
 
 /-! ### next? -/