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