From e3947cbe208a09775bb5ec1a4dc18ea484241a68 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 21 Aug 2025 11:08:31 +1000
Subject: [PATCH] chore: remove bad Option grind annotation (#10000)

This PR removes a `grind` annotation that fired on all `Option.map`s,
causing an avalanche of instantiations.
---
 src/Init/Data/Option/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 3f7f61d684..9e2e6f0393 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -345,7 +345,7 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 @[simp] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
   funext; simp [map_id']
 
-@[grind =] theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
+theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
 
 @[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
     (o.map f).get h = f (o.get (by simpa using h)) := by