From c8dae31ba5342cd5b07411a53b6d5490c955ea0e Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 14 Aug 2025 21:08:05 +1000
Subject: [PATCH] feat: review of `grind` annotations for `Option` (#9863)

This PR reviews `grind` annotations for `Option`, preferring to use
`@[grind =]` instead of `@[grind]` (and fixing a few problems revealed
by this), and making sure `@[grind =]` theorems are "fully applied".
---
 src/Init/Data/Option/Lemmas.lean | 158 +++++++++++++++++--------------
 tests/lean/run/grind_list2.lean  |  10 +-
 tests/lean/run/grind_option.lean |   7 +-
 3 files changed, 99 insertions(+), 76 deletions(-)

diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 9b429b16a8..3f7f61d684 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -58,9 +58,9 @@ theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.get
 theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b) := by
   cases o <;> simp
 
-@[simp, grind] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
+@[simp, grind =] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
 
-@[simp, grind] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
+@[simp, grind =] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
 
 theorem get_eq_get! [Inhabited α] : (o : Option α) → {h : o.isSome} → o.get h = o.get!
   | some _, _ => rfl
@@ -120,7 +120,7 @@ theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome :
 @[simp] theorem isNone_eq_false_iff : isNone a = false ↔ a.isSome = true := by
   cases a <;> simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem not_isSome (a : Option α) : (!a.isSome) = a.isNone := by
   cases a <;> simp
 
@@ -129,7 +129,7 @@ theorem not_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by
   funext
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem not_isNone (a : Option α) : (!a.isNone) = a.isSome := by
   cases a <;> simp
 
@@ -191,11 +191,15 @@ 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, grind] theorem pure_def : pure = @some α := rfl
+@[simp] theorem pure_def : pure = @some α := rfl
 
-@[simp, grind] theorem bind_eq_bind : bind = @Option.bind α β := rfl
+@[grind =] theorem pure_apply : pure x = some x := rfl
 
-@[simp, grind] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
+@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
+
+@[grind =] theorem bind_apply : bind x f = Option.bind x f := 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
@@ -216,7 +220,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]
 
-@[grind] 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
 
@@ -224,7 +228,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]
+@[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
 
@@ -232,12 +236,12 @@ 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]
+@[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]
+@[grind =]
 theorem isNone_bind {α β : Type _} (x : Option α) (f : α → Option β) :
     (x.bind f).isNone = x.all (fun x => (f x).isNone) := by
   cases x <;> rfl
@@ -250,7 +254,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, grind] 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
@@ -263,7 +267,7 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
     (o.bind f).all p = o.all (Option.all p ∘ f) := by
   cases o <;> simp
 
-@[grind] 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
 
 theorem join_eq_some_iff : x.join = some a ↔ x = some (some a) := by
   simp [← bind_id_eq_join, bind_eq_some_iff]
@@ -287,7 +291,9 @@ theorem bind_join {f : α → Option β} {o : Option (Option α)} :
     o.join.bind f = o.bind (·.bind f) := by
   cases o <;> simp
 
-@[simp, grind] theorem map_eq_map : Functor.map f = Option.map f := rfl
+@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl
+
+@[grind =] theorem map_apply : Functor.map f x = Option.map f x := rfl
 
 @[deprecated map_none (since := "2025-04-10")]
 abbrev map_none' := @map_none
@@ -313,13 +319,13 @@ abbrev map_eq_none := @map_eq_none_iff
 @[deprecated map_eq_none_iff (since := "2025-04-10")]
 abbrev map_eq_none' := @map_eq_none_iff
 
-@[simp, grind] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
+@[simp, grind =] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
   cases x <;> simp
 
 @[deprecated isSome_map (since := "2025-04-10")]
 abbrev isSome_map' := @isSome_map
 
-@[simp, grind] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
+@[simp, grind =] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
   cases x <;> simp
 
 theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by
@@ -329,28 +335,32 @@ 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, grind] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
+@[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
   funext; simp [map_id]
 
+@[grind =] theorem map_id_apply {α : Type u} {x : Option α} : Option.map (id : α → α) x = x := by simp
+
 theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 
-@[simp, grind] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
+@[simp] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
   funext; simp [map_id']
 
-@[simp, grind] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
+@[grind =] 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
   cases o with
   | none => simp at h
   | some a => simp
 
-@[simp, grind _=_] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
+@[simp] 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, ·∘·]
 
 theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h :=
   (map_map ..).symm
 
-@[simp, grind _=_] theorem map_comp_map (f : α → β) (g : β → γ) :
+@[simp] 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 ..
@@ -372,9 +382,9 @@ theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y
      (if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none := by
   split <;> rfl
 
-@[simp, grind] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
+@[simp, grind =] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
 
-@[grind] theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
+@[grind =] theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
 
 theorem filter_some_pos (h : p a) : Option.filter p (some a) = some a := by
   rw [filter_some, if_pos h]
@@ -417,12 +427,12 @@ theorem filter_some_eq_some : Option.filter p (some a) = some a ↔ p a := by si
 
 theorem filter_some_eq_none : Option.filter p (some a) = none ↔ ¬p a := by simp
 
-@[grind]
+@[grind =]
 theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
     a ∈ o.filter p ↔ a ∈ o ∧ p a := by
   simp
 
-@[grind]
+@[grind =]
 theorem bind_guard (x : Option α) (p : α → Bool) :
     x.bind (Option.guard p) = x.filter p := by
   cases x <;> rfl
@@ -457,7 +467,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
     | false => by simp [filter_some_neg h, h]
     | true => by simp [filter_some_pos h, h]
 
-@[simp, grind] theorem isSome_filter : Option.isSome (Option.filter p o) = Option.any p o :=
+@[simp, grind =] theorem isSome_filter : Option.isSome (Option.filter p o) = Option.any p o :=
   match o with
   | none => rfl
   | some a =>
@@ -536,12 +546,12 @@ theorem get_of_any_eq_true (p : α → Bool) (x : Option α) (h : x.any p = true
     p (x.get (isSome_of_any h)) :=
   any_eq_true_iff_get p x |>.1 h |>.2
 
-@[grind]
+@[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]
+@[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
@@ -549,13 +559,13 @@ theorem all_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
 
-@[grind] 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, grind] 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
 
-@[grind] 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
 
 @[grind _=_] theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
@@ -652,10 +662,11 @@ theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
   simp only [guard]
   split <;> simp
 
-@[grind]
 theorem guard_def (p : α → Bool) :
     Option.guard p = fun x => if p x then some x else none := rfl
 
+@[grind =] theorem guard_apply : Option.guard p x = if p x then some x else none := rfl
+
 @[deprecated guard_def (since := "2025-05-15")]
 theorem guard_eq_map (p : α → Bool) :
     Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
@@ -704,13 +715,13 @@ theorem merge_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b
   | none, some _ => .inr rfl
   | some a, some b => by have := h a b; simp [merge] at this ⊢; exact this
 
-@[simp, grind] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
+@[simp, grind =] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
   cases b <;> rfl
 
-@[simp, grind] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
+@[simp, grind =] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
   cases a <;> rfl
 
-@[simp, grind] theorem merge_some_some {f} {a b : α} :
+@[simp, grind =] theorem merge_some_some {f} {a b : α} :
   merge f (some a) (some b) = some (f a b) := rfl
 
 @[deprecated merge_eq_or_eq (since := "2025-04-04")]
@@ -784,9 +795,9 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
     (o.merge f o').get h = f (o.getD i) (o'.getD i) := by
   cases o <;> cases o' <;> simp [Std.LawfulLeftIdentity.left_id, Std.LawfulRightIdentity.right_id]
 
-@[simp, grind] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
+@[simp, grind =] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
-@[simp, grind] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
+@[simp, grind =] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
 @[grind =] theorem elim_filter {o : Option α} {b : β} :
     Option.elim (Option.filter p o) b f = Option.elim o b (fun a => if p a then f a else b) :=
@@ -804,7 +815,8 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
 theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
   cases h : p a <;> simp [*, guard]
 
-@[simp, grind] theorem getD_map (f : α → β) (x : α) (o : Option α) :
+-- I don't see how to construct a good grind pattern to instantiate this.
+@[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
 
 section choice
@@ -867,37 +879,37 @@ theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_c
 
 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 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
+@[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
-@[simp, grind] theorem none_or : none.or o = o := rfl
+@[simp, grind =] theorem some_or : (some a).or o = some a := rfl
+@[simp, grind =] theorem none_or : none.or o = o := rfl
 
 theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
   cases h; simp
 
-@[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]
+@[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
   cases o <;> rfl
 
-@[simp, grind] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
+@[simp, grind =] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
   cases o <;> rfl
 
-@[simp, grind] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
+@[simp, grind =] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
   cases o <;> rfl
 
 @[simp] theorem or_eq_none_iff : or o o' = none ↔ o = none ∧ o' = none := by
@@ -912,7 +924,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
 
-@[grind] 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 _⟩
 
@@ -923,7 +935,7 @@ instance : Std.LawfulIdentity (or (α := α)) none where
   left_id := @none_or _
   right_id := @or_none _
 
-@[simp, grind]
+@[simp, grind =]
 theorem or_self : or o o = o := by
   cases o <;> rfl
 instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
@@ -962,13 +974,15 @@ theorem guard_or_guard : (guard p a).or (guard q a) = guard (fun x => p x || q x
 /-! ### `orElse` -/
 
 /-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`. -/
-@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
+@[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
+
+@[grind =] theorem orElse_apply : HOrElse.hOrElse o o' = Option.orElse o o' := rfl
 
 theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
   cases o <;> rfl
 
 /-- The `simp` normal form of `o.orElse f` is o.or (f ())`. -/
-@[simp, grind] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
+@[simp, grind =] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
   simp [or_eq_orElse]
 
 @[deprecated or_some (since := "2025-05-03")]
@@ -1001,13 +1015,13 @@ section beq
 
 variable [BEq α]
 
-@[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
+@[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
+@[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
@@ -1128,12 +1142,15 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
 @[simp] theorem isSome_dite {p : Prop} {_ : Decidable p} {b : p → β} :
     (if h : p then some (b h) else none).isSome = true ↔ p := by
   split <;> simpa
+
 @[simp] theorem isSome_ite {p : Prop} {_ : Decidable p} :
     (if p then some b else none).isSome = true ↔ p := by
   split <;> simpa
+
 @[simp] theorem isSome_dite' {p : Prop} {_ : Decidable p} {b : ¬ p → β} :
     (if h : p then none else some (b h)).isSome = true ↔ ¬ p := by
   split <;> simpa
+
 @[simp] theorem isSome_ite' {p : Prop} {_ : Decidable p} :
     (if p then none else some b).isSome = true ↔ ¬ p := by
   split <;> simpa
@@ -1145,9 +1162,11 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
   · exfalso
     simp at w
     contradiction
+
 @[simp] theorem get_ite {p : Prop} {_ : Decidable p} (h) :
     (if p then some b else none).get h = b := by
   simpa using get_dite (p := p) (fun _ => b) (by simpa using h)
+
 @[simp] theorem get_dite' {p : Prop} {_ : Decidable p} (b : ¬ p → β) (w) :
     (if h : p then none else some (b h)).get w = b (by simpa using w) := by
   split
@@ -1155,13 +1174,14 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
     simp at w
     contradiction
   · simp
+
 @[simp] theorem get_ite' {p : Prop} {_ : Decidable p} (h) :
     (if p then none else some b).get h = b := by
   simpa using get_dite' (p := p) (fun _ => b) (by simpa using h)
 
 end ite
 
-@[simp, grind] 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
@@ -1176,16 +1196,16 @@ end ite
 @[grind = gen] theorem pbind_none' (h : x = none) : pbind x f = none := by subst h; rfl
 @[grind = gen] theorem pbind_some' (h : x = some a) : pbind x f = f a h := by subst h; rfl
 
-@[simp, grind] 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, grind] 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
 
-@[simp, grind] theorem pbind_eq_bind {α β : Type _} (o : Option α)
+@[simp] theorem pbind_eq_bind {α β : Type _} (o : Option α)
     (f : α → Option β) : o.pbind (fun x _ => f x) = o.bind f := by
   cases o <;> rfl
 
@@ -1253,11 +1273,11 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
     pmap f o h = none ↔ o = none := by
   cases o <;> simp
 
-@[simp, grind] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+@[simp, grind =] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
     (pmap f o h).isSome = o.isSome := by
   cases o <;> simp
 
-@[simp, grind] theorem isNone_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+@[simp, grind =] theorem isNone_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
     (pmap f o h).isNone = o.isNone := by
   cases o <;> simp
 
@@ -1279,11 +1299,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
 
-@[grind] 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
 
-@[grind] 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
@@ -1340,7 +1360,7 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
 @[simp] 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 α)
+@[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
@@ -1387,11 +1407,11 @@ theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
   congr; funext a ha
   exact hf a ha
 
-@[simp, grind] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
+@[simp, grind =] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
     none.pfilter p = none := by
   rfl
 
-@[simp, grind] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
+@[simp, grind =] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
     (some x).pfilter p = if p x rfl then some x else none := by
   simp only [pfilter, cond_eq_if]
 
@@ -1416,7 +1436,7 @@ theorem isNone_pfilter_iff {o : Option α} {p : (a : α) → o = some a → Bool
       Bool.not_eq_true, some.injEq]
     exact ⟨fun h _ h' => h' ▸ h, fun h => h _ rfl⟩
 
-@[simp, grind] 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/tests/lean/run/grind_list2.lean b/tests/lean/run/grind_list2.lean
index 47ea0cd484..b3c903eaf2 100644
--- a/tests/lean/run/grind_list2.lean
+++ b/tests/lean/run/grind_list2.lean
@@ -468,9 +468,10 @@ theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
 theorem map_eq_foldr {f : α → β} {l : List α} : map f l = foldr (fun a bs => f a :: bs) [] l := by
   induction l <;> grind
 
+attribute [local ext, local grind ext] List.ext_getElem in
 theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
     (l.set i a).map f = (l.map f).set i (f a) := by
-  grind +extAll
+  grind
 
 theorem head_map {f : α → β} {l : List α} (w) :
     (map f l).head w = f (l.head (by grind)) := by
@@ -489,8 +490,8 @@ theorem map_tail {f : α → β} {l : List α} :
 theorem headD_map {f : α → β} {l : List α} {a : α} : (map f l).headD (f a) = f (l.headD a) := by
   cases l with grind
 
-theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
-  grind
+-- theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
+--   grind
 
 theorem map_map {g : β → γ} {f : α → β} {l : List α} :
     map g (map f l) = map (g ∘ f) l := by induction l with grind
@@ -850,8 +851,9 @@ theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
       l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a := by
   grind [append_eq_replicate_iff]
 
+attribute [local ext, local grind ext] List.ext_getElem in
 theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
-  grind +extAll
+  grind
 
 theorem filter_replicate_of_pos (h : p a) : (replicate n a).filter p = replicate n a := by grind
 
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
index e36cf83b09..914467f78c 100644
--- a/tests/lean/run/grind_option.lean
+++ b/tests/lean/run/grind_option.lean
@@ -7,7 +7,8 @@ section
 variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}
 
 /--
-info: Try this: grind only [Option.some_or, Option.or_assoc, Option.some_beq_none, Option.or_some]
+info: Try this: grind only [=_ Option.or_assoc, = Option.getD_or, = Option.or_some, = Option.some_beq_none, = Option.or_assoc,
+  = Option.some_or]
 -/
 #guard_msgs in
 example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by grind?
@@ -16,11 +17,11 @@ 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_def] -/
+/-- info: Try this: grind only [= Option.guard_apply] -/
 #guard_msgs in
 example : Option.guard (· ≤ 7) 3 = some 3 := by grind?
 
-/-- info: Try this: grind only [Option.mem_bind_iff] -/
+/-- 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?