fix

leanprover-community · Aug 25, 2024 · 74dc3f9 · 74dc3f9
1 parent a37f19c
commit 74dc3f9
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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