diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index ae715b4ab8..dcd128dc8f 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -91,8 +91,6 @@ theorem eq_some_unique {o : Option α} {a b : α} (ha : o = some a) (hb : o = so
   | some _, _, H => ((H _).1 rfl).symm
   | _, some _, H => (H _).2 rfl
 
-set_option Elab.async false
-
 theorem eq_none_iff_forall_ne_some : o = none ↔ ∀ a, o ≠ some a := by
   cases o <;> simp
 
@@ -174,13 +172,13 @@ theorem forall_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x)
 @[deprecated forall_ne_none (since := "2025-04-04")]
 abbrev ball_ne_none := @forall_ne_none
 
-@[simp] theorem pure_def : pure = @some α := rfl
+@[simp, grind] theorem pure_def : pure = @some α := rfl
 
-@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
+@[simp, grind] theorem bind_eq_bind : bind = @Option.bind α β := rfl
 
-@[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
+@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
 
-@[simp] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
+@[simp, grind] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
 
 @[simp] theorem bind_fun_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
   cases x <;> rfl
@@ -201,7 +199,7 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
     o.bind f = none ↔ ∀ b a, o = some a → f a ≠ some b := by
   cases o <;> simp [eq_none_iff_forall_ne_some]
 
-theorem mem_bind_iff {o : Option α} {f : α → Option β} :
+@[grind] theorem mem_bind_iff {o : Option α} {f : α → Option β} :
     b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
   cases o <;> simp
 
@@ -209,6 +207,7 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
     (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
   cases a <;> cases b <;> rfl
 
+@[grind]
 theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
     (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
 
@@ -216,10 +215,16 @@ theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
     (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
   cases o <;> simp
 
+@[grind]
 theorem isSome_bind {α β : Type _} (x : Option α) (f : α → Option β) :
     (x.bind f).isSome = x.any (fun x => (f x).isSome) := by
   cases x <;> rfl
 
+@[grind]
+theorem isNone_bind {α β : Type _} (x : Option α) (f : α → Option β) :
+    (x.bind f).isNone = x.all (fun x => (f x).isNone) := by
+  cases x <;> rfl
+
 theorem isSome_of_isSome_bind {α β : Type _} {x : Option α} {f : α → Option β}
     (h : (x.bind f).isSome) : x.isSome := by
   cases x <;> trivial
@@ -228,7 +233,7 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
     (h : (x.bind f).isSome) : (f (x.get (isSome_of_isSome_bind h))).isSome := by
   cases x <;> trivial
 
-@[simp] theorem get_bind {α β : Type _} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome) :
+@[simp, grind] theorem get_bind {α β : Type _} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome) :
     (x.bind f).get h = (f (x.get (isSome_of_isSome_bind h))).get
       (isSome_apply_of_isSome_bind h) := by
   cases x <;> trivial
@@ -251,9 +256,9 @@ theorem join_eq_none_iff : o.join = none ↔ o = none ∨ o = some none :=
 @[deprecated join_eq_none_iff (since := "2025-04-10")]
 abbrev join_eq_none := @join_eq_none_iff
 
-theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
+@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
 
-@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl
+@[simp, grind] theorem map_eq_map : Functor.map f = Option.map f := rfl
 
 @[deprecated map_none (since := "2025-04-10")]
 abbrev map_none' := @map_none
@@ -316,7 +321,7 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h :=
   (map_map ..).symm
 
-@[simp] theorem map_comp_map (f : α → β) (g : β → γ) :
+@[simp, grind _=_] theorem map_comp_map (f : α → β) (g : β → γ) :
     Option.map g ∘ Option.map f = Option.map (g ∘ f) := by funext x; simp
 
 theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some ..
@@ -373,6 +378,7 @@ abbrev filter_eq_none := @filter_eq_none_iff
 @[deprecated filter_eq_some_iff (since := "2025-04-10")]
 abbrev filter_eq_some := @filter_eq_some_iff
 
+@[grind]
 theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
     a ∈ o.filter p ↔ a ∈ o ∧ p a := by
   simp
@@ -425,10 +431,16 @@ theorem any_eq_false_iff_get (p : α → Bool) (x : Option α) :
 theorem isSome_of_any {x : Option α} {p : α → Bool} (h : x.any p) : x.isSome := by
   cases x <;> trivial
 
+@[grind]
 theorem any_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
     (x.map f).any p = x.any (fun a => p (f a)) := by
   cases x <;> rfl
 
+@[grind]
+theorem all_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
+    (x.map f).all p = x.all (fun a => p (f a)) := by
+  cases x <;> rfl
+
 theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
     x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
 
@@ -462,7 +474,7 @@ theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
 theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none ↔ o = none ∧ f () = none := by
   cases o <;> simp
 
-@[grind]theorem map_orElse {x : Option α} {y} :
+@[grind] theorem map_orElse {x : Option α} {y} :
     (x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by
   cases x <;> simp
 
@@ -515,6 +527,7 @@ theorem guard_eq_map (p : α → Bool) :
   funext x
   simp [Option.guard]
 
+@[grind]
 theorem guard_def (p : α → Bool) :
     Option.guard p = fun x => if p x then some x else none := rfl
 
@@ -614,10 +627,15 @@ end choice
 theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
   cases h; simp
 
-@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
-
 /-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
-@[simp, grind] theorem or_some' {o : Option α} : o.or (some a) = some (o.getD a) := by
+@[simp, grind] theorem or_some {o : Option α} : o.or (some a) = some (o.getD a) := by
+  cases o <;> rfl
+
+@[deprecated or_some (since := "2025-05-03")]
+abbrev or_some' := @or_some
+
+@[simp, grind]
+theorem or_none : or o none = o := by
   cases o <;> rfl
 
 theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
@@ -645,10 +663,6 @@ abbrev or_eq_some := @or_eq_some_iff
   cases o₁ <;> cases o₂ <;> rfl
 instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
 
-@[simp, grind]
-theorem or_none : or o none = o := by
-  cases o <;> rfl
-
 theorem or_eq_left_of_none {o o' : Option α} (h : o' = none) : o.or o' = o := by
   cases h; simp
 
@@ -838,7 +852,7 @@ end ite
     (o.map f).pbind g = o.pbind (fun x h => g (f x) (h ▸ rfl)) := by
   cases o <;> rfl
 
-@[simp] theorem pbind_eq_bind {α β : Type _} (o : Option α)
+@[simp, grind] theorem pbind_eq_bind {α β : Type _} (o : Option α)
     (f : α → Option β) : o.pbind (fun x _ => f x) = o.bind f := by
   cases o <;> rfl
 
@@ -898,7 +912,7 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
     · rintro ⟨h, rfl⟩
       rfl
 
-@[simp]
+@[simp, grind]
 theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
     @pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
   cases o <;> simp
@@ -946,7 +960,7 @@ theorem pmap_congr {α : Type u} {β : Type v}
 @[simp, grind] theorem pelim_none : pelim none b f = b := rfl
 @[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
 
-@[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
+@[simp, grind] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp
 
 @[simp, grind] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
@@ -1004,7 +1018,7 @@ theorem pfilter_eq_some_iff {α : Type _} {o : Option α} {p : (a : α) → o =
   · rintro ⟨⟨h, rfl⟩, h'⟩
     exact ⟨⟨o.get h, ⟨h, rfl⟩, h'⟩, rfl⟩
 
-@[simp] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α → Bool} :
+@[simp, grind] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α → Bool} :
     o.pfilter (fun a _ => p a) = o.filter p := by
   cases o with
   | none => rfl
@@ -1020,13 +1034,13 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
 
 /-! ### LT and LE -/
 
-@[simp] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
-@[simp] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
-@[simp] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt]
+@[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
+@[simp, grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
+@[simp, grind] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt]
 
-@[simp] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]
-@[simp] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
-@[simp] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
+@[simp, grind] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]
+@[simp, grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
+@[simp, grind] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
 
 /-! ### min and max -/
 
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 6b49954cea..510013d94a 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -3255,11 +3255,11 @@ theorem getEntry?_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((
     · simp
     · cases hc : containsKey hd l
       · simp only [Bool.not_false, Bool.and_self, ↓reduceIte, Option.some_or, cond_true,
-          Option.or_some', Option.some.injEq]
+          Option.or_some, Option.some.injEq]
         rw [getEntry?_eq_none.2, Option.getD_none]
         rwa [← containsKey_congr hhd]
       · simp only [Bool.not_true, Bool.and_false, Bool.false_eq_true, ↓reduceIte, cond_true,
-          Option.or_some', getEntry?_eq_none]
+          Option.or_some, getEntry?_eq_none]
         rw [containsKey_congr hhd, containsKey_eq_isSome_getEntry?] at hc
         obtain ⟨v, hv⟩ := Option.isSome_iff_exists.1 hc
         simp [hv]
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
index 29563c5869..179295be9f 100644
--- a/tests/lean/run/grind_option.lean
+++ b/tests/lean/run/grind_option.lean
@@ -7,7 +7,7 @@ set_option grind.warning false
 variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}
 
 /--
-info: Try this: grind only [Option.some_or, Option.or_some', Option.or_assoc, Option.some_beq_none]
+info: Try this: grind only [Option.or_some, Option.some_or, Option.or_assoc, Option.some_beq_none]
 -/
 #guard_msgs in
 example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by grind?
@@ -16,6 +16,10 @@ example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by
 #guard_msgs in
 example : max (some 7) none = min (some 13) (some 7) := by grind?
 
-/-- info: Try this: grind only [Option.guard_pos] -/
+/-- info: Try this: grind only [Option.guard_def] -/
 #guard_msgs in
-example : Option.guard (· ≤ 7) 3 = some 3 := by grind? [Option.guard_pos]
+example : Option.guard (· ≤ 7) 3 = some 3 := by grind?
+
+/-- info: Try this: grind only [Option.mem_bind_iff] -/
+#guard_msgs in
+example {x : β} {o : Option α} {f : α → Option β} (h : a ∈ o) (h' : x ∈ f a) : x ∈ o.bind f := by grind?