diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 1f2abed5d8..79c28a44f4 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -479,7 +479,7 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
     · simp only [take_succ_cons, findIdx?_cons]
       split
       · simp
-      · simp [ih, Option.guard_comp]
+      · simp [ih, Option.guard_comp, Option.bind_map]
 
 @[simp] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
     min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 7f6b0497b4..4dcf3070af 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -248,7 +248,7 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
 theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
     x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
 
-@[simp] theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
+theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
     (x.map f).bind g = x.bind (g ∘ f) := by cases x <;> simp
 
 @[simp] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :