diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index 2efb75853d..dbe6cddff1 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -195,7 +195,7 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
   | some a =>
     simp only [filter_some, attach_some]
     ext
-    simp only [attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
+    simp only [attach_eq_some_iff, ite_none_right_eq_some, some.injEq, bind_some,
       dite_none_right_eq_some]
     constructor
     · rintro ⟨h, w⟩
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index dc481e9433..f127e4a537 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -13,11 +13,20 @@ namespace Option
 deriving instance DecidableEq for Option
 deriving instance BEq for Option
 
+@[simp, grind] theorem getD_none : getD none a = a := rfl
+@[simp, grind] theorem getD_some : getD (some a) b = a := rfl
+
+@[simp, grind] theorem map_none (f : α → β) : none.map f = none := rfl
+@[simp, grind] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
+
 /-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/
 def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
+@[simp, grind] theorem getM_none [Alternative m] : getM none = (failure : m α) := rfl
+@[simp, grind] theorem getM_some [Alternative m] {a : α} : getM (some a) = (pure a : m α) := rfl
+
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
@@ -75,6 +84,14 @@ Examples:
   | none,   _ => none
   | some a, f => f a
 
+@[simp, grind] theorem bind_none (f : α → Option β) : none.bind f = none := rfl
+@[simp, grind] theorem bind_some (a) (f : α → Option β) : (some a).bind f = f a := rfl
+
+@[deprecated bind_none (since := "2025-05-03")]
+abbrev none_bind := @bind_none
+@[deprecated bind_some (since := "2025-05-03")]
+abbrev some_bind := @bind_some
+
 /--
 Runs the monadic action `f` on `o`'s value, if any, and returns the result, or  `none` if there is
 no value.
@@ -102,6 +119,9 @@ This function only requires `m` to be an applicative functor. An alias `Option.m
   | none => pure none
   | some x => some <$> f x
 
+@[simp, grind] theorem mapM_none [Applicative m] (f : α → m β) : none.mapM f = pure none := rfl
+@[simp, grind] theorem mapM_some [Applicative m] (x) (f : α → m β) : (some x).mapM f = some <$> f x := rfl
+
 /--
 Applies a function in some applicative functor to an optional value, returning `none` with no
 effects if the value is missing.
@@ -111,6 +131,10 @@ This is an alias for `Option.mapM`, which already works for applicative functors
 @[inline] protected def mapA [Applicative m] (f : α → m β) : Option α → m (Option β) :=
   Option.mapM f
 
+/-- For verification purposes, we replace `mapA` with `mapM`. -/
+@[simp, grind] theorem mapA_eq_mapM [Applicative m] {f : α → m β} : Option.mapA f o = Option.mapM f o := rfl
+
+@[simp, grind]
 theorem map_id : (Option.map id : Option α → Option α) = id :=
   funext (fun o => match o with | none => rfl | some _ => rfl)
 
@@ -142,6 +166,9 @@ Examples:
   | some a => p a
   | none   => true
 
+@[simp, grind] theorem all_none : Option.all p none = true := rfl
+@[simp, grind] theorem all_some : Option.all p (some x) = p x := rfl
+
 /--
 Checks whether an optional value is not `none` and satisfies a Boolean predicate.
 
@@ -154,6 +181,9 @@ Examples:
   | some a => p a
   | none   => false
 
+@[simp, grind] theorem any_none : Option.any p none = false := rfl
+@[simp, grind] theorem any_some : Option.any p (some x) = p x := rfl
+
 /--
 Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
 `some a`, otherwise evaluates and returns the second argument.
@@ -164,6 +194,9 @@ See also `or` for a version that is strict in the second argument.
   | some a, _ => some a
   | none,   b => b ()
 
+@[simp, grind] theorem orElse_some : (some a).orElse b = some a := rfl
+@[simp, grind] theorem orElse_none : none.orElse b = b () := rfl
+
 instance : OrElse (Option α) where
   orElse := Option.orElse
 
@@ -230,15 +263,6 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
   | none  , some y => some y
   | some x, some y => some <| fn x y
 
-@[simp, grind] theorem getD_none : getD none a = a := rfl
-@[simp, grind] theorem getD_some : getD (some a) b = a := rfl
-
-@[simp, grind] theorem map_none (f : α → β) : none.map f = none := rfl
-@[simp, grind] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
-
-@[simp, grind] theorem none_bind (f : α → Option β) : none.bind f = none := rfl
-@[simp, grind] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl
-
 /--
 A case analysis function for `Option`.
 
@@ -262,9 +286,9 @@ Extracts the value from an option that can be proven to be `some`.
 @[inline] def get {α : Type u} : (o : Option α) → isSome o → α
   | some x, _ => x
 
-@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
+@[simp, grind] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
 | some _, _ => rfl
-@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
+@[simp, grind] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
 
 /--
 Returns `none` if a value doesn't satisfy a Boolean predicate, or the value itself otherwise.
@@ -342,6 +366,9 @@ Examples:
 -/
 @[simp, inline] def join (x : Option (Option α)) : Option α := x.bind id
 
+@[simp, grind] theorem join_none : (none : Option (Option α)).join = none := rfl
+@[simp, grind] theorem join_some : (some o).join = o := rfl
+
 /--
 Converts an optional monadic computation into a monadic computation of an optional value.
 
@@ -363,7 +390,10 @@ some "world"
 -/
 @[inline] def sequence [Applicative m] {α : Type u} : Option (m α) → m (Option α)
   | none => pure none
-  | some fn => some <$> fn
+  | some f => some <$> f
+
+@[simp, grind] theorem sequence_none [Applicative m] : (none : Option (m α)).sequence = pure none := rfl
+@[simp, grind] theorem sequence_some [Applicative m] (f : m (Option α)) : (some f).sequence = some <$> f := rfl
 
 /--
 A monadic case analysis function for `Option`.
@@ -388,6 +418,9 @@ This is the monadic analogue of `Option.getD`.
   | some a => pure a
   | none => y
 
+@[simp, grind] theorem getDM_none [Pure m] (y : m α) : (none : Option α).getDM y = y := rfl
+@[simp, grind] theorem getDM_some [Pure m] (a : α) (y : m α) : (some a).getDM y = pure a := rfl
+
 instance (α) [BEq α] [ReflBEq α] : ReflBEq (Option α) where
   rfl {x} :=
     match x with
@@ -400,12 +433,6 @@ instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
     | some x, some y => rw [LawfulBEq.eq_of_beq (α := α) h]
     | none, none => rfl
 
-@[simp, grind] theorem all_none : Option.all p none = true := rfl
-@[simp, grind] theorem all_some : Option.all p (some x) = p x := rfl
-
-@[simp, grind] theorem any_none : Option.any p none = false := rfl
-@[simp, grind] theorem any_some : Option.any p (some x) = p x := rfl
-
 /--
 The minimum of two optional values, with `none` treated as the least element. This function is
 usually accessed through the `Min (Option α)` instance, rather than directly.
@@ -428,10 +455,10 @@ protected def min [Min α] : Option α → Option α → Option α
 
 instance [Min α] : Min (Option α) where min := Option.min
 
-@[simp] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
-@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = none := rfl
-@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl
-@[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
+@[simp, grind] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
+@[simp, grind] theorem min_some_none [Min α] {a : α} : min (some a) none = none := rfl
+@[simp, grind] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl
+@[simp, grind] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
 
 /--
 The maximum of two optional values.
@@ -453,10 +480,10 @@ protected def max [Max α] : Option α → Option α → Option α
 
 instance [Max α] : Max (Option α) where max := Option.max
 
-@[simp] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl
-@[simp] theorem max_some_none [Max α] {a : α} : max (some a) none = some a := rfl
-@[simp] theorem max_none_some [Max α] {b : α} : max none (some b) = some b := rfl
-@[simp] theorem max_none_none [Max α] : max (none : Option α) none = none := rfl
+@[simp, grind] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl
+@[simp, grind] theorem max_some_none [Max α] {a : α} : max (some a) none = some a := rfl
+@[simp, grind] theorem max_none_some [Max α] {b : α} : max none (some b) = some b := rfl
+@[simp, grind] theorem max_none_none [Max α] : max (none : Option α) none = none := rfl
 
 
 end Option
@@ -481,6 +508,7 @@ instance : Alternative Option where
   failure := Option.none
   orElse  := Option.orElse
 
+-- This is a duplicate of `Option.getM`; one may be deprecated in the future.
 def liftOption [Alternative m] : Option α → m α
   | some a => pure a
   | none   => failure
diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean
index 06fa8a4e0b..816869adf9 100644
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -12,7 +12,7 @@ universe u v
 
 namespace Option
 
-theorem eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀z, x = some z ↔ y = some z) → x = y
+theorem eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀ z, x = some z ↔ y = some z) → x = y
   | none,   none,   _ => rfl
   | none,   some z, h => Option.noConfusion ((h z).2 rfl)
   | some z, none,   h => Option.noConfusion ((h z).1 rfl)
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 618e9533a4..ae715b4ab8 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -180,9 +180,9 @@ abbrev ball_ne_none := @forall_ne_none
 
 @[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
 
-@[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl
+@[simp] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
 
-@[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
+@[simp] theorem bind_fun_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
   cases x <;> rfl
 
 theorem bind_eq_some_iff : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
@@ -295,21 +295,21 @@ theorem map_congr {x : Option α} (h : ∀ a, x = some a → f a = g a) :
     x.map f = x.map g := by
   cases x <;> simp only [map_none, map_some, h]
 
-@[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
+@[simp, grind] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
   funext; simp [map_id]
 
 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
+@[simp, grind] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
   funext; simp [map_id']
 
-theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
+@[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
   cases o with
   | none => simp at h
   | some a => simp
 
-@[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
+@[simp, grind _=_] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
     (x.map g).map h = x.map (h ∘ g) := by
   cases x <;> simp only [map_none, map_some, ·∘·]
 
@@ -381,12 +381,12 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     x.filter p = x.bind (Option.guard p) := by
   cases x <;> rfl
 
-@[simp] theorem all_guard (a : α) :
+@[simp, grind] theorem all_guard (a : α) :
     Option.all q (guard p a) = (!p a || q a) := by
   simp only [guard]
   split <;> simp_all
 
-@[simp] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
+@[simp, grind] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
   simp only [guard]
   split <;> simp_all
 
@@ -432,26 +432,28 @@ theorem any_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Boo
 theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
     x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
 
-theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
+@[grind] 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 α} :
+@[simp, grind] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
     (x.bind f).map g = x.bind (Option.map g ∘ f) := by cases x <;> simp
 
-theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
+@[grind] theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
     (x.map (Option.map f)).join = x.join.map f := by cases x <;> simp
 
-theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
+@[grind _=_] theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
   cases x <;> simp
 
 theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x :=
   h.symm ▸ join_eq_some_iff.1 h
 
-@[simp, grind] theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
+@[deprecated orElse_some (since := "2025-05-03")]
+theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
 
-@[simp, grind] theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
+@[deprecated orElse_none (since := "2025-05-03")]
+theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
 
-@[simp] theorem orElse_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
+@[simp] theorem orElse_fun_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
 
 theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
     (o.orElse f) = some x ↔ o = some x ∨ o = none ∧ f () = some x := by
@@ -460,7 +462,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
 
-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
 
@@ -504,7 +506,7 @@ theorem guard_comp {p : α → Bool} {f : β → α} :
   ext1 b
   simp [guard]
 
-theorem bind_guard (x : Option α) (p : α → Bool) :
+@[grind] theorem bind_guard (x : Option α) (p : α → Bool) :
     x.bind (Option.guard p) = x.filter p := by
   simp only [Option.filter_eq_bind, decide_eq_true_eq]
 
@@ -599,9 +601,11 @@ abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
 end choice
 
 @[simp, grind] theorem toList_some (a : α) : (some a).toList = [a] := rfl
-
 @[simp, grind] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
 
+@[simp, grind] theorem toArray_some (a : α) : (some a).toArray = #[a] := rfl
+@[simp, grind] theorem toArray_none (α : Type _) : (none : Option α).toArray = #[] := rfl
+
 -- See `Init.Data.Option.List` for lemmas about `toList`.
 
 @[simp, grind] theorem some_or : (some a).or o = some a := rfl
@@ -637,7 +641,7 @@ abbrev or_eq_none := @or_eq_none_iff
 @[deprecated or_eq_some_iff (since := "2025-04-10")]
 abbrev or_eq_some := @or_eq_some_iff
 
-theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
+@[grind] theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
   cases o₁ <;> cases o₂ <;> rfl
 instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
 
@@ -685,10 +689,14 @@ section beq
 
 variable [BEq α]
 
-@[simp] theorem none_beq_none : ((none : Option α) == none) = true := rfl
-@[simp] theorem none_beq_some (a : α) : ((none : Option α) == some a) = false := rfl
-@[simp] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl
-@[simp] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl
+@[simp, grind] theorem none_beq_none : ((none : Option α) == none) = true := rfl
+@[simp, grind] theorem none_beq_some (a : α) : ((none : Option α) == some a) = false := rfl
+@[simp, grind] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl
+@[simp, grind] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl
+
+/-- We simplify away `isEqSome` in terms of `==`. -/
+@[simp, grind] theorem isEqSome_eq_beq_some {o : Option α} : isEqSome o y = (o == some y) := by
+  cases o <;> simp [isEqSome]
 
 @[simp] theorem reflBEq_iff : ReflBEq (Option α) ↔ ReflBEq α := by
   constructor
@@ -802,14 +810,14 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
 
 end ite
 
-theorem isSome_filter {α : Type _} {x : Option α} {f : α → Bool} :
+@[grind] theorem isSome_filter {α : Type _} {x : Option α} {f : α → Bool} :
     (x.filter f).isSome = x.any f := by
   cases x
   · rfl
   · rw [Bool.eq_iff_iff]
     simp only [Option.any_some, Option.filter, Option.isSome_ite]
 
-@[simp] theorem get_filter {α : Type _} {x : Option α} {f : α → Bool} (h : (x.filter f).isSome) :
+@[simp, grind] theorem get_filter {α : Type _} {x : Option α} {f : α → Bool} (h : (x.filter f).isSome) :
     (x.filter f).get h = x.get (isSome_of_isSome_filter f x h) := by
   cases x
   · contradiction
@@ -821,11 +829,11 @@ theorem isSome_filter {α : Type _} {x : Option α} {f : α → Bool} :
 @[simp, grind] theorem pbind_none : pbind none f = none := rfl
 @[simp, grind] theorem pbind_some : pbind (some a) f = f a rfl := rfl
 
-@[simp] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
+@[simp, grind] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     {g : β → γ} : (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
   cases o <;> rfl
 
-@[simp] theorem pbind_map {α β γ : Type _} (o : Option α)
+@[simp, grind] theorem pbind_map {α β γ : Type _} (o : Option α)
     (f : α → β) (g : (x : β) → o.map f = some x → Option γ) :
     (o.map f).pbind g = o.pbind (fun x h => g (f x) (h ▸ rfl)) := by
   cases o <;> rfl
@@ -895,11 +903,11 @@ 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
 
-theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
+@[grind] theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
     Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
   cases o <;> simp
 
-theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
+@[grind] theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
     pmap g (o.map f) H =
       pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some_iff.2 ⟨_, m, rfl⟩)) := by
   cases o <;> simp
@@ -941,7 +949,7 @@ theorem pmap_congr {α : Type u} {β : Type v}
 @[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp
 
-@[simp] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
+@[simp, grind] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
     (H : ∀ (a : α), o = some a → p a) (g : γ) (g' : β → γ) :
     (o.pmap f H).elim g g' =
        o.pelim g (fun a h => g' (f a (H a h))) := by
@@ -978,7 +986,7 @@ theorem isSome_of_isSome_pfilter {α : Type _} {o : Option α} {p : (a : α) →
     (h : (o.pfilter p).isSome) : o.isSome :=
   (isSome_pfilter_iff_get.mp h).1
 
-@[simp] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
+@[simp, grind] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
     (h : (o.pfilter p).isSome) :
     (o.pfilter p).get h = o.get (isSome_of_isSome_pfilter h) := by
   cases o <;> simp
diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean
index 23989ab347..5553f47d11 100644
--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -10,62 +10,38 @@ import Init.Data.List.Lemmas
 
 namespace Option
 
-@[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ o = some a := by
+@[simp, grind] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ o = some a := by
   cases o <;> simp [eq_comm]
 
-@[simp] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
-    forIn' none b f = pure b := by
-  rfl
-
-@[simp] theorem forIn'_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
-    forIn' (some a) b f = bind (f a rfl b) (fun r => pure (ForInStep.value r)) := by
-  simp only [forIn', bind_pure_comp]
-  rw [map_eq_pure_bind]
-  congr
-  funext x
-  split <;> rfl
-
-@[simp] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
-    forIn none b f = pure b := by
-  rfl
-
-@[simp] theorem forIn_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn (some a) b f = bind (f a b) (fun r => pure (ForInStep.value r)) := by
-  simp only [forIn, forIn', bind_pure_comp]
-  rw [map_eq_pure_bind]
-  congr
-  funext x
-  split <;> rfl
-
-@[simp] theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
+@[simp, grind] theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
     forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b := by
   cases o <;> rfl
 
-@[simp] theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
+@[simp, grind] theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn o.toList b f = forIn o b f := by
   cases o <;> rfl
 
-@[simp] theorem foldlM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
+@[simp, grind] theorem foldlM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
     o.toList.foldlM f a = o.elim (pure a) (fun b => f a b) := by
   cases o <;> simp
 
-@[simp] theorem foldrM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
+@[simp, grind] theorem foldrM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
     o.toList.foldrM f a = o.elim (pure a) (fun b => f b a) := by
   cases o <;> simp
 
-@[simp] theorem foldl_toList (o : Option β) (a : α) (f : α → β → α) :
+@[simp, grind] theorem foldl_toList (o : Option β) (a : α) (f : α → β → α) :
     o.toList.foldl f a = o.elim a (fun b => f a b) := by
   cases o <;> simp
 
-@[simp] theorem foldr_toList (o : Option β) (a : α) (f : β → α → α) :
+@[simp, grind] theorem foldr_toList (o : Option β) (a : α) (f : β → α → α) :
     o.toList.foldr f a = o.elim a (fun b => f b a) := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind]
 theorem pairwise_toList {P : α → α → Prop} {o : Option α} : o.toList.Pairwise P := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind]
 theorem head?_toList {o : Option α} : o.toList.head? = o := by
   cases o <;> simp
 
diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean
index 32e36e11e4..3281db7249 100644
--- a/src/Init/Data/Option/Monadic.lean
+++ b/src/Init/Data/Option/Monadic.lean
@@ -12,16 +12,47 @@ import Init.Control.Lawful.Basic
 
 namespace Option
 
-@[simp] theorem forM_none [Monad m] (f : α → m PUnit) :
-    none.forM f = pure .unit := rfl
+@[simp, grind] theorem bindM_none [Monad m] (f : α → m (Option β)) : none.bindM f = pure none := rfl
+@[simp, grind] theorem bindM_some [Monad m] [LawfulMonad m] (a) (f : α → m (Option β)) : (some a).bindM f = f a := by
+  simp [Option.bindM]
 
-@[simp] theorem forM_some [Monad m] (f : α → m PUnit) (a : α) :
-    (some a).forM f = f a := rfl
+-- We simplify `Option.forM` to `forM`.
+@[simp] theorem forM_eq_forM [Monad m] : @Option.forM m α _ = forM := rfl
 
-@[simp] theorem forM_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit) :
-    (o.map g).forM f = o.forM (fun a => f (g a)) := by
+@[simp, grind] theorem forM_none [Monad m] (f : α → m PUnit) :
+    forM none f = pure .unit := rfl
+
+@[simp, grind] theorem forM_some [Monad m] (f : α → m PUnit) (a : α) :
+    forM (some a) f = f a := rfl
+
+@[simp, grind] theorem forM_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit) :
+    forM (o.map g) f = forM o (fun a => f (g a)) := by
   cases o <;> simp
 
+@[simp, grind] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
+    forIn' none b f = pure b := by
+  rfl
+
+@[simp, grind] theorem forIn'_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
+    forIn' (some a) b f = bind (f a rfl b) (fun r => pure (ForInStep.value r)) := by
+  simp only [forIn', bind_pure_comp]
+  rw [map_eq_pure_bind]
+  congr
+  funext x
+  split <;> rfl
+
+@[simp, grind] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
+    forIn none b f = pure b := by
+  rfl
+
+@[simp, grind] theorem forIn_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
+    forIn (some a) b f = bind (f a b) (fun r => pure (ForInStep.value r)) := by
+  simp only [forIn, forIn', bind_pure_comp]
+  rw [map_eq_pure_bind]
+  congr
+  funext x
+  split <;> rfl
+
 @[congr] theorem forIn'_congr [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs)
     {b b' : β} (hb : b = b')
     {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
@@ -60,7 +91,7 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
       o.pelim b (fun a h => f a h b) := by
   cases o <;> simp
 
-@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
+@[simp, grind] theorem forIn'_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
     forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y := by
   cases o <;> simp
@@ -89,11 +120,9 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
       o.elim b (fun a => f a b) := by
   cases o <;> simp
 
-@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
+@[simp, grind] theorem forIn_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
     forIn (o.map g) init f = forIn o init fun a y => f (g a) y := by
   cases o <;> simp
 
-@[simp] theorem mapA_eq_mapM : @Option.mapA = @Option.mapM := rfl
-
 end Option
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 7548c70ca6..6b49954cea 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -4495,10 +4495,10 @@ theorem getEntry?_filterMap' [BEq α] [EquivBEq α]
     specialize hf ⟨k', v⟩
     split
     · rename_i h
-      simp only [List.filterMap_cons, Option.some_bind]
+      simp only [List.filterMap_cons, Option.bind_some]
       simp only [containsKey_congr h] at hl
       split
-      · simp only [ih, ‹f _ = _›, Option.none_bind, getEntry?_eq_none.mpr hl.2]
+      · simp only [ih, ‹f _ = _›, Option.bind_none, getEntry?_eq_none.mpr hl.2]
       · rw [‹f _ = _›, Option.all_some, BEq.congr_right h] at hf
         rw [getEntry?_cons, hf, ‹f _ = _›, cond_true]
     · simp only [List.filterMap_cons]
@@ -5169,7 +5169,7 @@ theorem getValue?_filterMap_of_getKey?_eq_some {β : Type v} {γ : Type w} [BEq
   simp only [getKey?_eq_getEntry?, Option.map_eq_some_iff, getValue?_eq_getEntry?,
     getEntry?_filterMap distinct, Option.map_bind, forall_exists_index, and_imp]
   intro x hx hk
-  simp only [hx, Option.some_bind, Function.comp_apply, hk, Option.map_map, Option.map_some]
+  simp only [hx, Option.bind_some, Function.comp_apply, hk, Option.map_map, Option.map_some]
   cases f k' x.2 <;> simp
 
 theorem getValue!_filterMap {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] [Inhabited γ]
diff --git a/tests/lean/grind/experiments/option.lean b/tests/lean/grind/experiments/option.lean
deleted file mode 100644
index 76abcd5ef2..0000000000
--- a/tests/lean/grind/experiments/option.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-/-!
-This file contains WIP notes about potential further `grind` attributes for `Option`.
-
--/
-
-attribute [grind] Option.some_get Option.get_some
-attribute [grind] Option.map_map -- `[grind _=_]`?
-attribute [grind] Option.get_map -- ??
-attribute [grind] Option.map_id_fun Option.map_id_fun'
-attribute [grind] Option.all_guard Option.any_guard
-attribute [grind] Option.bind_map Option.map_bind
-attribute [grind] Option.join_map_eq_map_join
-attribute [grind] Option.join_join -- `[grind _=_]`?
-attribute [grind] Option.map_orElse
-
--- Look again at `Option.guard` lemmas, consider `bind_gaurd`.
--- Fix statement of `isSome_guard`, add `isNone_guard`
-
-attribute [grind] Option.or_assoc -- unless `grind` gains native associativity support in the meantime!
-
--- attribute [grind] Option.none_beq_none -- warning: this generates just `none` as the pattern!
--- attribute [grind] Option.none_beq_some
--- attribute [grind] Option.some_beq_none -- warning: this generates just `some _` as the pattern!
--- attribute [grind] Option.some_beq_some
-
-attribute [grind] Option.isSome_filter
-attribute [grind] Option.get_filter Option.get_pfilter
-
-attribute [grind] Option.map_pbind Option.pbind_map
-attribute [grind] Option.map_pmap Option.pmap_map Option.elim_pmap
-
--- Lemmas about inequalities?
-
--- The `min_none_none` family of lemmas result in grind issues:
--- failed to synthesize instance when instantiating Option.min_none_none
---         Min α
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
new file mode 100644
index 0000000000..29563c5869
--- /dev/null
+++ b/tests/lean/run/grind_option.lean
@@ -0,0 +1,21 @@
+-- This file uses `#guard_msgs` to check which lemmas `grind` is using.
+-- This may prove fragile, so remember it is okay to update the expected output if appropriate!
+-- Hopefully these will act as regression tests against `grind` activating irrelevant lemmas.
+
+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]
+-/
+#guard_msgs in
+example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by grind?
+
+/-- info: Try this: grind only [= Nat.min_def, Option.max_some_none, Option.min_some_some] -/
+#guard_msgs in
+example : max (some 7) none = min (some 13) (some 7) := by grind?
+
+/-- info: Try this: grind only [Option.guard_pos] -/
+#guard_msgs in
+example : Option.guard (· ≤ 7) 3 = some 3 := by grind? [Option.guard_pos]