From c96fbdda44c14c7c256f046fb2b71fae25ea968e Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 9 Sep 2024 16:05:06 +1000
Subject: [PATCH] chore: remove @[simp] from List.head_mem and similar (#5271)

These attributes do not seem particularly useful after all.
---
 src/Init/Data/List/Find.lean   | 2 +-
 src/Init/Data/List/Lemmas.lean | 4 ++--
 tests/lean/run/list_simp.lean  | 3 ---
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 771a3dd41b..d98de43397 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -266,7 +266,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
     · exact H ▸ .head _
     · exact .tail _ (mem_of_find?_eq_some H)
 
-@[simp] theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h ∈ xs := by
+theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h ∈ xs := by
   induction xs with
   | nil => simp at h
   | cons x xs ih =>
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 713def2ac2..fd3ea85c1d 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -900,7 +900,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
 
-@[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
   | [], h => absurd rfl h
   | [_], _ => .head ..
   | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
@@ -989,7 +989,7 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
 @[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
   cases l <;> simp
 
-@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
+theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
   | [], h => absurd rfl h
   | _::_, _ => .head ..
 
diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean
index 93d97c8fe9..e62eb854d1 100644
--- a/tests/lean/run/list_simp.lean
+++ b/tests/lean/run/list_simp.lean
@@ -61,9 +61,6 @@ variable (m n : Nat)
 
 #check_simp l.head? = none ~> l = []
 
-variable (w : l ≠ []) in
-#check_simp l.head w ∈ l ~> True
-
 /-! ### tail!, tail?, tailD -/
 
 /-! ## Basic operations -/