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

@@ -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 =>

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 ..
 

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 -/