From 74dc3f9df45b8768b3662c978c25cdf9de8f17b1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 25 Aug 2024 21:40:41 +1000
Subject: [PATCH] fix

---
 Mathlib/Data/List/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index 849703ac0ada9..cfff858ee4d5a 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -368,7 +368,8 @@ lemma getLast_filter {p : α → Bool} :
 
 /-! ### getLast? -/
 
-@[simp]
+-- This is a duplicate of `getLast?_eq_none_iff`.
+-- We should remove one of them.
 theorem getLast?_eq_none : ∀ {l : List α}, getLast? l = none ↔ l = []
   | [] => by simp
   | [a] => by simp