diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index c94b09a0f5f9..58370f3c86df 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -34,7 +34,7 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
     · exact H ▸ h
     · exact find?_some H
 
-@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
+theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ .head _