From 4dbd20343f9e6ccbdf59bbb93dc097ce77e7df4b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 21 Aug 2024 13:16:22 +1000
Subject: [PATCH] chore: remove @[simp] from mem_of_find?_eq_some (#5105)

---
 src/Init/Data/List/Find.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index c94b09a0f5..58370f3c86 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 _