diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 6c1469d7a3..dc6e9625e7 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -197,7 +197,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp, grind =] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean
index 5052e310bd..2773f41e12 100644
--- a/src/Init/Data/Array/Erase.lean
+++ b/src/Init/Data/Array/Erase.lean
@@ -91,7 +91,7 @@ theorem mem_of_mem_eraseP {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseP
 
-@[simp, grind] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
+@[simp, grind =] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_eraseP_of_neg pa
 
@@ -240,7 +240,7 @@ theorem mem_of_mem_erase {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a 
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_erase (by simpa using h)
 
-@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
+@[simp, grind =] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
     a ∈ xs.erase b ↔ a ∈ xs :=
   erase_eq_eraseP b xs ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index fcb75f2794..f1b26f1553 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -27,8 +27,8 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
-@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind =] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp, grind =] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp [List.findSome?_append]
 
 @[grind =]
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 47e02d19b2..f228abdd7e 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -211,7 +211,7 @@ theorem ext_getElem? {xs ys : Array α} (h : ∀ i : Nat, xs[i]? = ys[i]?) : xs
 
 @[simp] theorem pop_push {xs : Array α} {x : α} : (xs.push x).pop = xs := by simp [pop]
 
-@[simp, grind] theorem getElem_pop {xs : Array α} {i : Nat} (h : i < xs.pop.size) :
+@[simp, grind =] theorem getElem_pop {xs : Array α} {i : Nat} (h : i < xs.pop.size) :
     xs.pop[i] = xs[i]'(by simp at h; omega) := by
   rcases xs with ⟨xs⟩
   simp [List.getElem_dropLast]
@@ -331,7 +331,7 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by
 
 /-! ### replicate -/
 
-@[simp, grind] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
+@[simp, grind =] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
   List.length_replicate ..
 
 @[deprecated size_replicate (since := "2025-03-18")]
@@ -343,7 +343,7 @@ abbrev size_mkArray := @size_replicate
 @[deprecated toList_replicate (since := "2025-03-18")]
 abbrev toList_mkArray := @toList_replicate
 
-@[simp, grind] theorem replicate_zero : replicate 0 a = #[] := rfl
+@[simp, grind =] theorem replicate_zero : replicate 0 a = #[] := rfl
 
 @[deprecated replicate_zero (since := "2025-03-18")]
 abbrev mkArray_zero := @replicate_zero
@@ -356,7 +356,7 @@ theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
 @[deprecated replicate_succ (since := "2025-03-18")]
 abbrev mkArray_succ := @replicate_succ
 
-@[simp, grind] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
+@[simp, grind =] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
     (replicate n v)[i] = v := by simp [← getElem_toList]
 
 @[deprecated getElem_replicate (since := "2025-03-18")]
@@ -521,7 +521,7 @@ theorem forall_getElem {xs : Array α} {p : α → Prop} :
 /-! ### isEmpty -/
 
 @[grind =] theorem isEmpty_empty : (#[] : Array α).isEmpty = true := rfl
-@[simp, grind] theorem isEmpty_push {xs : Array α} : (xs.push x).isEmpty = false := by
+@[simp, grind =] theorem isEmpty_push {xs : Array α} : (xs.push x).isEmpty = false := by
   rcases xs with ⟨xs⟩
   simp
 
@@ -860,14 +860,14 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as)
 theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = decide (a ∈ xs) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
+@[simp, grind =] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]
 
 @[grind =] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
 @[grind =] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
-@[simp, grind] theorem any_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
+@[simp, grind =] theorem any_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
     (xs.push a).any p 0 stop = (xs.any p || p a) := by
   cases xs
   rw [List.push_toArray]
@@ -878,7 +878,7 @@ theorem any_push {xs : Array α} {a : α} {p : α → Bool} :
   any_push' (by simp)
 
 /-- Variant of `all_push` with a side condition on `stop`. -/
-@[simp, grind] theorem all_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
+@[simp, grind =] theorem all_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
     (xs.push a).all p 0 stop = (xs.all p && p a) := by
   cases xs
   rw [List.push_toArray]
@@ -983,7 +983,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 
 /-! ### setIfInBounds -/
 
-@[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
+@[simp, grind =] theorem setIfInBounds_empty {i : Nat} {a : α} :
     #[].setIfInBounds i a = #[] := rfl
 
 @[simp, grind =] theorem set!_eq_setIfInBounds : set! xs i v = setIfInBounds xs i v := rfl
@@ -992,7 +992,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
     xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl
 
-@[simp, grind] theorem size_setIfInBounds {xs : Array α} {i : Nat} {a : α} :
+@[simp, grind =] theorem size_setIfInBounds {xs : Array α} {i : Nat} {a : α} :
     (xs.setIfInBounds i a).size = xs.size := by
   if h : i < xs.size  then
     simp [setIfInBounds, h]
@@ -1082,11 +1082,11 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
-@[simp, grind] theorem beq_empty_eq [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
+@[simp, grind =] theorem beq_empty_eq [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
   cases xs
   simp
 
-@[simp, grind] theorem empty_beq_eq [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
+@[simp, grind =] theorem empty_beq_eq [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
   cases xs
   simp
 
@@ -1096,7 +1096,7 @@ abbrev beq_empty_iff := @beq_empty_eq
 @[deprecated empty_beq_eq (since := "2025-04-04")]
 abbrev empty_beq_iff := @empty_beq_eq
 
-@[simp, grind] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
+@[simp, grind =] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
   cases ys
@@ -1202,17 +1202,17 @@ where
   apply ext'
   simp
 
-@[simp, grind] theorem size_map {f : α → β} {xs : Array α} : (xs.map f).size = xs.size := by
+@[simp, grind =] theorem size_map {f : α → β} {xs : Array α} : (xs.map f).size = xs.size := by
   simp only [← length_toList]
   simp
 
 -- The argument `f : α → β` is explicit, to facilitate rewriting from right to left.
-@[simp, grind] theorem getElem_map (f : α → β) {xs : Array α} {i : Nat} (hi : i < (xs.map f).size) :
+@[simp, grind =] theorem getElem_map (f : α → β) {xs : Array α} {i : Nat} (hi : i < (xs.map f).size) :
     (xs.map f)[i] = f (xs[i]'(by simpa using hi)) := by
   cases xs
   simp
 
-@[simp, grind] theorem getElem?_map {f : α → β} {xs : Array α} {i : Nat} :
+@[simp, grind =] theorem getElem?_map {f : α → β} {xs : Array α} {i : Nat} :
     (xs.map f)[i]? = xs[i]?.map f := by
   simp [getElem?_def]
 
@@ -1222,7 +1222,7 @@ where
 
 @[grind =] theorem map_empty {f : α → β} : map f #[] = #[] := by simp
 
-@[simp, grind] theorem map_push {f : α → β} {as : Array α} {x : α} :
+@[simp, grind =] theorem map_push {f : α → β} {as : Array α} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
   ext
   · simp
@@ -1452,7 +1452,7 @@ grind_pattern Array.size_filter_le => (xs.filter p).size
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind] theorem mem_filter {p : α → Bool} {xs : Array α} {a : α} :
+@[simp, grind =] theorem mem_filter {p : α → Bool} {xs : Array α} {a : α} :
     a ∈ xs.filter p ↔ a ∈ xs ∧ p a := by
   rcases xs with ⟨xs⟩
   simp
@@ -1514,7 +1514,7 @@ theorem map_filter_eq_foldl {f : α → β} {p : α → Bool} {xs : Array α} :
     simp only [List.filter_cons, List.foldr_cons]
     split <;> simp_all
 
-@[simp, grind] theorem filter_append {p : α → Bool} {xs ys : Array α} {stop : Nat} (w : stop = xs.size + ys.size) :
+@[simp, grind =] theorem filter_append {p : α → Bool} {xs ys : Array α} {stop : Nat} (w : stop = xs.size + ys.size) :
     filter p (xs ++ ys) 0 stop = filter p xs ++ filter p ys := by
   subst w
   rcases xs with ⟨xs⟩
@@ -1568,7 +1568,7 @@ theorem size_filter_lt_size_iff_exists {xs : Array α} {p : α → Bool} :
 
 /-! ### filterMap -/
 
-@[simp, grind] theorem filterMap_empty {f : α → Option β} : filterMap f #[] = #[] := rfl
+@[simp, grind =] theorem filterMap_empty {f : α → Option β} : filterMap f #[] = #[] := rfl
 
 @[congr]
 theorem filterMap_congr {as bs : Array α} (h : as = bs)
@@ -1644,7 +1644,7 @@ theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
   cases xs
   simp
 
-@[simp, grind] theorem filterMap_some {xs : Array α} : filterMap some xs = xs := by
+@[simp, grind =] theorem filterMap_some {xs : Array α} : filterMap some xs = xs := by
   cases xs
   simp
 
@@ -1684,7 +1684,7 @@ theorem map_filterMap {f : α → Option β} {g : β → γ} {xs : Array α} :
   cases xs
   simp [List.map_filterMap]
 
-@[simp, grind] theorem filterMap_map {f : α → β} {g : β → Option γ} {xs : Array α} :
+@[simp, grind =] theorem filterMap_map {f : α → β} {g : β → Option γ} {xs : Array α} :
     filterMap g (map f xs) = filterMap (g ∘ f) xs := by
   cases xs
   simp [List.filterMap_map]
@@ -1699,7 +1699,7 @@ theorem filterMap_filter {p : α → Bool} {f : α → Option β} {xs : Array α
   cases xs
   simp [List.filterMap_filter]
 
-@[simp, grind] theorem mem_filterMap {f : α → Option β} {xs : Array α} {b : β} :
+@[simp, grind =] theorem mem_filterMap {f : α → Option β} {xs : Array α} {b : β} :
     b ∈ filterMap f xs ↔ ∃ a, a ∈ xs ∧ f a = some b := by
   simp only [mem_def, toList_filterMap, List.mem_filterMap]
 
@@ -1711,7 +1711,7 @@ theorem forall_mem_filterMap {f : α → Option β} {xs : Array α} {P : β →
   intro a
   rw [forall_comm]
 
-@[simp, grind] theorem filterMap_append {α β : Type _} {xs ys : Array α} {f : α → Option β}
+@[simp, grind =] theorem filterMap_append {α β : Type _} {xs ys : Array α} {f : α → Option β}
     {stop : Nat} (w : stop = xs.size + ys.size) :
     filterMap f (xs ++ ys) 0 stop = filterMap f xs ++ filterMap f ys := by
   subst w
@@ -1770,7 +1770,7 @@ theorem size_filterMap_lt_size_iff_exists {xs : Array α} {f : α → Option β}
 
 /-! ### append -/
 
-@[simp, grind] theorem size_append {xs ys : Array α} : (xs ++ ys).size = xs.size + ys.size := by
+@[simp, grind =] theorem size_append {xs ys : Array α} : (xs ++ ys).size = xs.size + ys.size := by
   simp only [size, toList_append, List.length_append]
 
 @[simp, grind _=_] theorem push_append {a : α} {xs ys : Array α} : (xs ++ ys).push a = xs ++ ys.push a := by
@@ -1807,7 +1807,7 @@ theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
   funext ⟨l⟩
   simp
 
-@[simp, grind] theorem mem_append {a : α} {xs ys : Array α} : a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys := by
+@[simp, grind =] theorem mem_append {a : α} {xs ys : Array α} : a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys := by
   simp only [mem_def, toList_append, List.mem_append]
 
 theorem mem_append_left {a : α} {xs : Array α} (ys : Array α) (h : a ∈ xs) : a ∈ xs ++ ys :=
@@ -2068,7 +2068,7 @@ theorem append_eq_filterMap_iff {f : α → Option β} :
       ∃ as bs, zs = as ++ bs ∧ filterMap f as = xs ∧ filterMap f bs = ys := by
   rw [eq_comm, filterMap_eq_append_iff]
 
-@[simp, grind] theorem map_append {f : α → β} {xs ys : Array α} :
+@[simp, grind =] theorem map_append {f : α → β} {xs ys : Array α} :
     map f (xs ++ ys) = map f xs ++ map f ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
@@ -2084,9 +2084,9 @@ theorem append_eq_map_iff {f : α → β} :
 
 /-! ### flatten -/
 
-@[simp, grind] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl
+@[simp, grind =] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl
 
-@[simp, grind] theorem toList_flatten {xss : Array (Array α)} :
+@[simp, grind =] theorem toList_flatten {xss : Array (Array α)} :
     xss.flatten.toList = (xss.toList.map toList).flatten := by
   dsimp [flatten]
   simp only [← foldl_toList]
@@ -2112,11 +2112,11 @@ theorem flatten_map_toArray {L : List (List α)} :
   apply ext'
   simp
 
-@[simp, grind] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by
+@[simp, grind =] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by
   cases xss using array₂_induction
   simp [Function.comp_def]
 
-@[simp, grind] theorem flatten_singleton {xs : Array α} : #[xs].flatten = xs := by simp [flatten]; rfl
+@[simp, grind =] theorem flatten_singleton {xs : Array α} : #[xs].flatten = xs := by simp [flatten]; rfl
 
 theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs, xs ∈ xss ∧ a ∈ xs := by
   simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]
@@ -2159,7 +2159,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap
       Function.comp_def]
     rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
-@[simp, grind] theorem filterMap_flatten {f : α → Option β} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
+@[simp, grind =] theorem filterMap_flatten {f : α → Option β} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filterMap f (flatten xss) 0 stop = flatten (map (filterMap f) xss) := by
   subst w
   induction xss using array₂_induction
@@ -2167,7 +2167,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap
     List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
-@[simp, grind] theorem filter_flatten {p : α → Bool} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
+@[simp, grind =] theorem filter_flatten {p : α → Bool} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filter p (flatten xss) 0 stop = flatten (map (filter p) xss) := by
   subst w
   induction xss using array₂_induction
@@ -2282,7 +2282,7 @@ theorem flatMap_def {xs : Array α} {f : α → Array β} : xs.flatMap f = flatt
   rcases xs with ⟨l⟩
   simp [flatten_toArray, Function.comp_def, List.flatMap_def]
 
-@[simp, grind] theorem flatMap_empty {β} {f : α → Array β} : (#[] : Array α).flatMap f = #[] := rfl
+@[simp, grind =] theorem flatMap_empty {β} {f : α → Array β} : (#[] : Array α).flatMap f = #[] := rfl
 
 theorem flatMap_toList {xs : Array α} {f : α → List β} :
     xs.toList.flatMap f = (xs.flatMap (fun a => (f a).toArray)).toList := by
@@ -2318,7 +2318,7 @@ theorem size_flatMap {xs : Array α} {f : α → Array β} :
   rcases xs with ⟨l⟩
   simp
 
-@[simp, grind] theorem mem_flatMap {f : α → Array β} {b} {xs : Array α} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
+@[simp, grind =] theorem mem_flatMap {f : α → Array β} {b} {xs : Array α} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
@@ -2346,7 +2346,7 @@ theorem flatMap_singleton {f : α → Array β} {x : α} : #[x].flatMap f = f x
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind] theorem flatMap_push {xs : Array α} {x : α} {f : α → Array β} :
+@[simp, grind =] theorem flatMap_push {xs : Array α} {x : α} {f : α → Array β} :
     (xs.push x).flatMap f = xs.flatMap f ++ f x := by
   rcases xs with ⟨xs⟩
   simp
@@ -2415,7 +2415,7 @@ theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate n a := by
 @[deprecated replicate_succ' (since := "2025-03-18")]
 abbrev mkArray_succ' := @replicate_succ'
 
-@[simp, grind] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+@[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
   simp only [mem_toArray, List.mem_replicate]
 
@@ -2637,7 +2637,7 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
 
 /-! ### reverse -/
 
-@[simp, grind] theorem size_reverse {xs : Array α} : xs.reverse.size = xs.size := by
+@[simp, grind =] theorem size_reverse {xs : Array α} : xs.reverse.size = xs.size := by
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
@@ -2646,7 +2646,7 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
     termination_by j - i
   simp only [reverse]; split <;> simp [go]
 
-@[simp, grind] theorem reverse_empty : reverse (#[] : Array α) = #[] := rfl
+@[simp, grind =] theorem reverse_empty : reverse (#[] : Array α) = #[] := rfl
 
 @[simp] theorem toList_reverse {xs : Array α} : xs.reverse.toList = xs.toList.reverse := by
   let rec go (as : Array α) (i j hj)
@@ -2701,7 +2701,7 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
   cases xs
   simp
 
-@[simp, grind] theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size) :
+@[simp, grind =] theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size) :
     (xs.reverse)[i] = xs[xs.size - 1 - i]'(by simp at hi; omega) := by
   cases xs
   simp
@@ -2730,14 +2730,14 @@ theorem getElem?_reverse' {xs : Array α} {i j} (h : i + j + 1 = xs.size) : xs.r
   simp only [List.reverse_toArray, List.getElem?_toArray]
   rw [List.getElem?_reverse' h]
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem?_reverse {xs : Array α} {i} (h : i < xs.size) :
     xs.reverse[i]? = xs[xs.size - 1 - i]? := by
   cases xs
   simp_all
 
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
-@[simp, grind] theorem reverse_reverse (xs : Array α) : xs.reverse.reverse = xs := by
+@[simp, grind =] theorem reverse_reverse (xs : Array α) : xs.reverse.reverse = xs := by
   cases xs
   simp
 
@@ -2776,7 +2776,7 @@ theorem reverse_eq_iff {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse
   cases xs
   simp
 
-@[simp, grind] theorem reverse_append {xs ys : Array α} : (xs ++ ys).reverse = ys.reverse ++ xs.reverse := by
+@[simp, grind =] theorem reverse_append {xs ys : Array α} : (xs ++ ys).reverse = ys.reverse ++ xs.reverse := by
   cases xs
   cases ys
   simp
@@ -2810,7 +2810,7 @@ theorem flatten_reverse {xss : Array (Array α)} :
   cases xs
   simp [List.flatMap_reverse, Function.comp_def]
 
-@[simp, grind] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
+@[simp, grind =] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
   rw [← toList_inj]
   simp
 
@@ -2971,10 +2971,10 @@ theorem extract_empty_of_size_le_start {xs : Array α} {start stop : Nat} (h : x
   simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
   rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero, extract_loop_zero]
 
-@[simp, grind] theorem extract_empty {start stop : Nat} : (#[] : Array α).extract start stop = #[] :=
+@[simp, grind =] theorem extract_empty {start stop : Nat} : (#[] : Array α).extract start stop = #[] :=
   extract_empty_of_size_le_start (Nat.zero_le _)
 
-@[simp, grind] theorem extract_zero {xs : Array α} : xs.extract start 0 = #[] := by
+@[simp, grind =] theorem extract_zero {xs : Array α} : xs.extract start 0 = #[] := by
   ext i h₁ h₂
   · simp
   · simp at h₁
@@ -3168,7 +3168,7 @@ theorem foldlM_append [Monad m] [LawfulMonad m] {f : β → α → m β} {b} {xs
     · rfl
     · simp at h₂
 
-@[simp, grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} {start stop : Nat} :
+@[simp, grind =] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} {start stop : Nat} :
     foldrM f init #[] start stop = return init := by
   simp [foldrM]
 
@@ -3242,6 +3242,7 @@ rather than `(arr.push a).size` as the argument.
     (xs.push a).foldrM f init start = f a init >>= xs.foldrM f := by
   simp [← foldrM_push, h]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
     l.foldrM (fun x xs => xs.push <$> f x) xs = do return xs ++ (← l.reverse.mapM f).toArray := by
   induction l with
@@ -3254,6 +3255,7 @@ rather than `(arr.push a).size` as the argument.
     funext x
     simp
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
     l.foldlM (fun xs x => xs.push <$> f x) xs = do return xs ++ (← l.mapM f).toArray := by
   induction l generalizing xs <;> simp [*]
@@ -3310,7 +3312,7 @@ theorem foldl_push {f : β → α → β} {init : β} {xs : Array α} {a : α} :
   foldlM_push ..
 
 /-- Variant of `foldl_push` with a side condition for the `stop` argument. -/
-@[simp, grind] theorem foldl_push' {f : β → α → β} {init : β} {xs : Array α} {a : α} {stop : Nat}
+@[simp, grind =] theorem foldl_push' {f : β → α → β} {init : β} {xs : Array α} {a : α} {stop : Nat}
     (h : stop = xs.size + 1) :
     (xs.push a).foldl f init 0 stop = f (xs.foldl f init) a := by
   subst h
@@ -3323,10 +3325,11 @@ theorem foldr_push {f : α → β → β} {init : β} {xs : Array α} {a : α} :
 Variant of `foldr_push` with the `h : start = arr.size + 1`
 rather than `(arr.push a).size` as the argument.
 -/
-@[simp, grind] theorem foldr_push' {f : α → β → β} {init : β} {xs : Array α} {a : α} {start : Nat}
+@[simp, grind =] theorem foldr_push' {f : α → β → β} {init : β} {xs : Array α} {a : α} {start : Nat}
     (h : start = xs.size + 1) : (xs.push a).foldr f init start = xs.foldr f (f a init) :=
   foldrM_push' h
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) :
     as.foldl (fun acc a => acc.push (f a)) bs 0 stop = bs ++ as.map f := by
   subst w
@@ -3335,12 +3338,14 @@ rather than `(arr.push a).size` as the argument.
   simp only [List.foldl_toArray']
   induction as generalizing bs <;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) :
     as.foldl (fun acc a => (f a) :: acc) bs 0 stop = (as.map f).reverse.toList ++ bs := by
   subst w
   rcases as with ⟨as⟩
   simp
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldr_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) :
     as.foldr (fun a acc => (f a) :: acc) bs start 0 = (as.map f).toList ++ bs := by
   subst w
@@ -3348,27 +3353,29 @@ rather than `(arr.push a).size` as the argument.
   simp
 
 /-- Variant of `foldr_cons_eq_append` specialized to `f = id`. -/
-@[simp, grind] theorem foldr_cons_eq_append' {as : Array α} {bs : List α} (w : start = as.size) :
+@[simp, grind =] theorem foldr_cons_eq_append' {as : Array α} {bs : List α} (w : start = as.size) :
     as.foldr List.cons bs start 0 = as.toList ++ bs := by
   subst w
   rcases as with ⟨as⟩
   simp
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
     l.foldr (fun x xs => xs.push (f x)) xs = xs ++ (l.reverse.map f).toArray := by
   induction l <;> simp [*]
 
 /-- Variant of `List.foldr_push_eq_append` specialized to `f = id`. -/
-@[simp, grind] theorem _root_.List.foldr_push_eq_append' {l : List α} {xs : Array α} :
+@[simp, grind =] theorem _root_.List.foldr_push_eq_append' {l : List α} {xs : Array α} :
     l.foldr (fun x xs => xs.push x) xs = xs ++ l.reverse.toArray := by
   induction l <;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
     l.foldl (fun xs x => xs.push (f x)) xs = xs ++ (l.map f).toArray := by
   induction l generalizing xs <;> simp [*]
 
 /-- Variant of `List.foldl_push_eq_append` specialized to `f = id`. -/
-@[simp, grind] theorem _root_.List.foldl_push_eq_append' {l : List α} {xs : Array α} :
+@[simp, grind =] theorem _root_.List.foldl_push_eq_append' {l : List α} {xs : Array α} :
     l.foldl (fun xs x => xs.push x) xs = xs ++ l.toArray := by
   simpa using List.foldl_push_eq_append (f := id)
 
@@ -3380,24 +3387,28 @@ theorem _root_.List.foldl_push {l : List α} {as : Array α} : l.foldl Array.pus
 theorem _root_.List.foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
   rw [List.foldr_eq_foldl_reverse, List.foldl_push_eq_append']
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldr_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (f · ++ ·) ys = (xs.map f).flatten ++ ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs <;> simp_all [Function.comp_def, flatten_toArray]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldl (· ++ f ·) ys = ys ++ (xs.map f).flatten := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs generalizing ys <;> simp_all [Function.comp_def, flatten_toArray]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldr_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (fun x acc => acc ++ f x) ys = ys ++ (xs.map f).reverse.flatten := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs generalizing ys <;> simp_all [Function.comp_def, flatten_toArray]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldl (fun acc y => f y ++ acc) ys = (xs.map f).reverse.flatten ++ ys:= by
   rcases xs with ⟨l⟩
@@ -3688,7 +3699,7 @@ theorem back_append_left {xs ys : Array α} (w : 0 < (xs ++ ys).size) (h : ys.si
   rw [List.getLast_append_left]
   simpa using h
 
-@[simp, grind] theorem back?_append {xs ys : Array α} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+@[simp, grind =] theorem back?_append {xs ys : Array α} : (xs ++ ys).back? = ys.back?.or xs.back? := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.back?_toArray]
@@ -4171,13 +4182,13 @@ theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
 section replace
 variable [BEq α]
 
-@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by simp [replace]
+@[simp, grind =] theorem replace_empty : (#[] : Array α).replace a b = #[] := by simp [replace]
 
-@[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
+@[simp, grind =] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
   simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
   by_cases h : a == b <;> simp [h]
 
-@[simp, grind] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
+@[simp, grind =] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
   simp only [replace]
   split <;> simp
 
@@ -4368,7 +4379,7 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 
 /-! ### sum -/
 
-@[simp, grind] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
+@[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
@@ -4441,7 +4452,7 @@ theorem getElem_mem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] 
 theorem back!_eq_back? [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD default := by
   simp [back!, back?, getElem!_def, Option.getD]; rfl
 
-@[simp, grind] theorem back?_push {xs : Array α} {x : α} : (xs.push x).back? = some x := by
+@[simp, grind =] theorem back?_push {xs : Array α} {x : α} : (xs.push x).back? = some x := by
   simp [back?]
 
 @[simp] theorem back!_push [Inhabited α] {xs : Array α} {x : α} : (xs.push x).back! = x := by
diff --git a/src/Init/Data/BitVec/Bootstrap.lean b/src/Init/Data/BitVec/Bootstrap.lean
index f4202ad18c..9c584195eb 100644
--- a/src/Init/Data/BitVec/Bootstrap.lean
+++ b/src/Init/Data/BitVec/Bootstrap.lean
@@ -19,7 +19,7 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 @[simp, grind =] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
-@[simp, grind] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
+@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
   let ⟨x, x_lt⟩ := x
   simp only [getLsbD_ofFin]
   apply Nat.testBit_lt_two_pow
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 49d585467e..d0b61a84ec 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -37,7 +37,7 @@ namespace BitVec
 @[simp] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
     (BitVec.ofFin x)[i] = x.val.testBit i := rfl
 
-@[simp, grind] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
+@[simp, grind =] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
   rw [getMsbD]
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index aea8ee06ab..a82aee8fcd 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -174,7 +174,7 @@ theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
-@[simp, grind]
+@[simp, grind =]
 theorem mem_attachWith {l : List α} {q : α → Prop} (H) (x : {x // q x}) :
     x ∈ l.attachWith q H ↔ x.1 ∈ l := by
   induction l with
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 90981520fb..2e942b0f03 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -80,17 +80,17 @@ namespace List
 
 /-! ### length -/
 
-@[simp, grind] theorem length_nil : length ([] : List α) = 0 :=
+@[simp, grind =] theorem length_nil : length ([] : List α) = 0 :=
   rfl
 
 @[simp] theorem length_singleton {a : α} : length [a] = 1 := rfl
 
-@[simp, grind] theorem length_cons {a : α} {as : List α} : (cons a as).length = as.length + 1 :=
+@[simp, grind =] theorem length_cons {a : α} {as : List α} : (cons a as).length = as.length + 1 :=
   rfl
 
 /-! ### set -/
 
-@[simp, grind] theorem length_set {as : List α} {i : Nat} {a : α} : (as.set i a).length = as.length := by
+@[simp, grind =] theorem length_set {as : List α} {i : Nat} {a : α} : (as.set i a).length = as.length := by
   induction as generalizing i with
   | nil => rfl
   | cons x xs ih =>
@@ -101,8 +101,8 @@ namespace List
 /-! ### foldl -/
 
 -- As `List.foldl` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
-@[simp, grind] theorem foldl_nil : [].foldl f b = b := rfl
-@[simp, grind] theorem foldl_cons {l : List α} {f : β → α → β} {b : β} : (a :: l).foldl f b = l.foldl f (f b a) := rfl
+@[simp, grind =] theorem foldl_nil : [].foldl f b = b := rfl
+@[simp, grind =] theorem foldl_cons {l : List α} {f : β → α → β} {b : β} : (a :: l).foldl f b = l.foldl f (f b a) := rfl
 
 /-! ### concat -/
 
@@ -332,7 +332,7 @@ def getLast? : List α → Option α
   | []    => none
   | a::as => some (getLast (a::as) (fun h => List.noConfusion h))
 
-@[simp, grind] theorem getLast?_nil : @getLast? α [] = none := rfl
+@[simp, grind =] theorem getLast?_nil : @getLast? α [] = none := rfl
 
 /-! ### getLastD -/
 
@@ -365,7 +365,7 @@ Returns the first element of a non-empty list.
 def head : (as : List α) → as ≠ [] → α
   | a::_, _ => a
 
-@[simp, grind] theorem head_cons {a : α} {l : List α} {h} : head (a::l) h = a := rfl
+@[simp, grind =] theorem head_cons {a : α} {l : List α} {h} : head (a::l) h = a := rfl
 
 /-! ### head? -/
 
@@ -383,8 +383,8 @@ def head? : List α → Option α
   | []   => none
   | a::_ => some a
 
-@[simp, grind] theorem head?_nil : head? ([] : List α) = none := rfl
-@[simp, grind] theorem head?_cons {a : α} {l : List α} : head? (a::l) = some a := rfl
+@[simp, grind =] theorem head?_nil : head? ([] : List α) = none := rfl
+@[simp, grind =] theorem head?_cons {a : α} {l : List α} : head? (a::l) = some a := rfl
 
 /-! ### headD -/
 
@@ -420,8 +420,8 @@ def tail : List α → List α
   | []    => []
   | _::as => as
 
-@[simp, grind] theorem tail_nil : tail ([] : List α) = [] := rfl
-@[simp, grind] theorem tail_cons {a : α} {as : List α} : tail (a::as) = as := rfl
+@[simp, grind =] theorem tail_nil : tail ([] : List α) = [] := rfl
+@[simp, grind =] theorem tail_cons {a : α} {as : List α} : tail (a::as) = as := rfl
 
 /-! ### tail? -/
 
@@ -441,8 +441,8 @@ def tail? : List α → Option (List α)
   | []    => none
   | _::as => some as
 
-@[simp, grind] theorem tail?_nil : tail? ([] : List α) = none := rfl
-@[simp, grind] theorem tail?_cons {a : α} {l : List α} : tail? (a::l) = some l := rfl
+@[simp, grind =] theorem tail?_nil : tail? ([] : List α) = none := rfl
+@[simp, grind =] theorem tail?_cons {a : α} {l : List α} : tail? (a::l) = some l := rfl
 
 /-! ### tailD -/
 
@@ -490,8 +490,8 @@ Examples:
   | []    => []
   | a::as => f a :: map f as
 
-@[simp, grind] theorem map_nil {f : α → β} : map f [] = [] := rfl
-@[simp, grind] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := rfl
+@[simp, grind =] theorem map_nil {f : α → β} : map f [] = [] := rfl
+@[simp, grind =] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := rfl
 
 /-! ### filter -/
 
@@ -511,7 +511,7 @@ def filter (p : α → Bool) : (l : List α) → List α
     | true => a :: filter p as
     | false => filter p as
 
-@[simp, grind] theorem filter_nil {p : α → Bool} : filter p [] = [] := rfl
+@[simp, grind =] theorem filter_nil {p : α → Bool} : filter p [] = [] := rfl
 
 /-! ### filterMap -/
 
@@ -537,7 +537,7 @@ Example:
     | none   => filterMap f as
     | some b => b :: filterMap f as
 
-@[simp, grind] theorem filterMap_nil {f : α → Option β} : filterMap f [] = [] := rfl
+@[simp, grind =] theorem filterMap_nil {f : α → Option β} : filterMap f [] = [] := rfl
 @[grind] theorem filterMap_cons {f : α → Option β} {a : α} {l : List α} :
     filterMap f (a :: l) =
       match f a with
@@ -561,8 +561,8 @@ Examples:
   | []     => init
   | a :: l => f a (foldr f init l)
 
-@[simp, grind] theorem foldr_nil : [].foldr f b = b := rfl
-@[simp, grind] theorem foldr_cons {a} {l : List α} {f : α → β → β} {b} :
+@[simp, grind =] theorem foldr_nil : [].foldr f b = b := rfl
+@[simp, grind =] theorem foldr_cons {a} {l : List α} {f : α → β → β} {b} :
     (a :: l).foldr f b = f a (l.foldr f b) := rfl
 
 /-! ### reverse -/
@@ -591,7 +591,7 @@ Examples:
 @[expose] def reverse (as : List α) : List α :=
   reverseAux as []
 
-@[simp, grind] theorem reverse_nil : reverse ([] : List α) = [] := rfl
+@[simp, grind =] theorem reverse_nil : reverse ([] : List α) = [] := rfl
 
 theorem reverseAux_reverseAux {as bs cs : List α} :
     reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs) := by
@@ -645,10 +645,10 @@ instance : Append (List α) := ⟨List.append⟩
 
 @[simp] theorem append_eq {as bs : List α} : List.append as bs = as ++ bs := rfl
 
-@[simp, grind] theorem nil_append (as : List α) : [] ++ as = as := rfl
+@[simp, grind =] theorem nil_append (as : List α) : [] ++ as = as := rfl
 @[simp, grind _=_] theorem cons_append {a : α} {as bs : List α} : (a::as) ++ bs = a::(as ++ bs) := rfl
 
-@[simp, grind] theorem append_nil (as : List α) : as ++ [] = as := by
+@[simp, grind =] theorem append_nil (as : List α) : as ++ [] = as := by
   induction as with
   | nil => rfl
   | cons a as ih =>
@@ -658,7 +658,7 @@ instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
   left_id := nil_append
   right_id := append_nil
 
-@[simp, grind] theorem length_append {as bs : List α} : (as ++ bs).length = as.length + bs.length := by
+@[simp, grind =] theorem length_append {as bs : List α} : (as ++ bs).length = as.length + bs.length := by
   induction as with
   | nil => simp
   | cons _ as ih => simp [ih, Nat.succ_add]
@@ -685,7 +685,7 @@ theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux a
     rw [ih (bs := a :: bs), ih (bs := [a]), append_assoc]
     rfl
 
-@[simp, grind] theorem reverse_cons {a : α} {as : List α} : reverse (a :: as) = reverse as ++ [a] := by
+@[simp, grind =] theorem reverse_cons {a : α} {as : List α} : reverse (a :: as) = reverse as ++ [a] := by
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
@@ -704,8 +704,8 @@ def flatten : List (List α) → List α
   | []      => []
   | l :: L => l ++ flatten L
 
-@[simp, grind] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
-@[simp, grind] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
+@[simp, grind =] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
+@[simp, grind =] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
 
 /-! ### singleton -/
 
@@ -731,8 +731,8 @@ Examples:
 -/
 @[inline] def flatMap {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List β := flatten (map b as)
 
-@[simp, grind] theorem flatMap_nil {f : α → List β} : List.flatMap f [] = [] := by simp [List.flatMap]
-@[simp, grind] theorem flatMap_cons {x : α} {xs : List α} {f : α → List β} :
+@[simp, grind =] theorem flatMap_nil {f : α → List β} : List.flatMap f [] = [] := by simp [List.flatMap]
+@[simp, grind =] theorem flatMap_cons {x : α} {xs : List α} {f : α → List β} :
   List.flatMap f (x :: xs) = f x ++ List.flatMap f xs := by simp [List.flatMap]
 
 /-! ### replicate -/
@@ -748,10 +748,10 @@ def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a
 
-@[simp, grind] theorem replicate_zero {a : α} : replicate 0 a = [] := rfl
+@[simp, grind =] theorem replicate_zero {a : α} : replicate 0 a = [] := rfl
 @[grind] theorem replicate_succ {a : α} {n : Nat} : replicate (n+1) a = a :: replicate n a := rfl
 
-@[simp, grind] theorem length_replicate {n : Nat} {a : α} : (replicate n a).length = n := by
+@[simp, grind =] theorem length_replicate {n : Nat} {a : α} : (replicate n a).length = n := by
   induction n with
   | zero => simp
   | succ n ih => simp only [ih, replicate_succ, length_cons]
@@ -819,8 +819,8 @@ def isEmpty : List α → Bool
   | []     => true
   | _ :: _ => false
 
-@[simp, grind] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
-@[simp, grind] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
+@[simp, grind =] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
+@[simp, grind =] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
 
 /-! ### elem -/
 
@@ -842,7 +842,7 @@ def elem [BEq α] (a : α) : (l : List α) → Bool
     | true  => true
     | false => elem a bs
 
-@[simp, grind] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
+@[simp, grind =] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
     (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
@@ -958,9 +958,9 @@ def take : (n : Nat) → (xs : List α) → List α
   | _+1, []    => []
   | n+1, a::as => a :: take n as
 
-@[simp, grind] theorem take_nil {i : Nat} : ([] : List α).take i = [] := by cases i <;> rfl
-@[simp, grind] theorem take_zero {l : List α} : l.take 0 = [] := rfl
-@[simp, grind] theorem take_succ_cons {a : α} {as : List α} {i : Nat} : (a::as).take (i+1) = a :: as.take i := rfl
+@[simp, grind =] theorem take_nil {i : Nat} : ([] : List α).take i = [] := by cases i <;> rfl
+@[simp, grind =] theorem take_zero {l : List α} : l.take 0 = [] := rfl
+@[simp, grind =] theorem take_succ_cons {a : α} {as : List α} {i : Nat} : (a::as).take (i+1) = a :: as.take i := rfl
 
 /-! ### drop -/
 
@@ -980,10 +980,10 @@ def drop : (n : Nat) → (xs : List α) → List α
   | _+1, []    => []
   | n+1, _::as => drop n as
 
-@[simp, grind] theorem drop_nil : ([] : List α).drop i = [] := by
+@[simp, grind =] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
-@[simp, grind] theorem drop_zero {l : List α} : l.drop 0 = l := rfl
-@[simp, grind] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := rfl
+@[simp, grind =] theorem drop_zero {l : List α} : l.drop 0 = l := rfl
+@[simp, grind =] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := rfl
 
 theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.drop i = [] := by
   match as, i with
@@ -1094,13 +1094,13 @@ def dropLast {α} : List α → List α
   | [_]   => []
   | a::as => a :: dropLast as
 
-@[simp, grind] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
-@[simp, grind] theorem dropLast_singleton : [x].dropLast = [] := rfl
+@[simp, grind =] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
+@[simp, grind =] theorem dropLast_singleton : [x].dropLast = [] := rfl
 
 @[deprecated dropLast_singleton (since := "2025-04-16")]
 theorem dropLast_single : [x].dropLast = [] := dropLast_singleton
 
-@[simp, grind] theorem dropLast_cons₂ :
+@[simp, grind =] theorem dropLast_cons₂ :
     (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
 
 -- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`,
@@ -1439,7 +1439,7 @@ def replace [BEq α] : (l : List α) → (a : α) → (b : α) → List α
     | true  => c::as
     | false => a :: replace as b c
 
-@[simp, grind] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
+@[simp, grind =] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
 @[grind] theorem replace_cons [BEq α] {a : α} :
     (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
@@ -1648,7 +1648,7 @@ def findSome? (f : α → Option β) : List α → Option β
     | some b => some b
     | none   => findSome? f as
 
-@[simp, grind] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
+@[simp, grind =] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
 @[grind] theorem findSome?_cons {f : α → Option β} :
     (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
   rfl
@@ -1906,8 +1906,8 @@ def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
 
-@[simp, grind] theorem any_nil : [].any f = false := rfl
-@[simp, grind] theorem any_cons : (a::l).any f = (f a || l.any f) := rfl
+@[simp, grind =] theorem any_nil : [].any f = false := rfl
+@[simp, grind =] theorem any_cons : (a::l).any f = (f a || l.any f) := rfl
 
 /-! ### all -/
 
@@ -1925,8 +1925,8 @@ def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
 
-@[simp, grind] theorem all_nil : [].all f = true := rfl
-@[simp, grind] theorem all_cons : (a::l).all f = (f a && l.all f) := rfl
+@[simp, grind =] theorem all_nil : [].all f = true := rfl
+@[simp, grind =] theorem all_cons : (a::l).all f = (f a && l.all f) := rfl
 
 /-! ### or -/
 
@@ -2066,8 +2066,8 @@ Examples:
 def sum {α} [Add α] [Zero α] : List α → α :=
   foldr (· + ·) 0
 
-@[simp, grind] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
-@[simp, grind] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+@[simp, grind =] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
+@[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
 /-! ### range -/
 
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 79446b4b03..e10f36e5f1 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -130,7 +130,7 @@ theorem le_length_eraseP {l : List α} : l.length - 1 ≤ (l.eraseP p).length :=
 @[grind →]
 theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset ·)
 
-@[simp, grind] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
+@[simp, grind =] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
   refine ⟨mem_of_mem_eraseP, fun al => ?_⟩
   match exists_or_eq_self_of_eraseP p l with
   | .inl h => rw [h]; assumption
@@ -393,7 +393,7 @@ theorem le_length_erase [LawfulBEq α] {a : α} {l : List α} : l.length - 1 ≤
 @[grind →]
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset h
 
-@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
+@[simp, grind =] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
     a ∈ l.erase b ↔ a ∈ l :=
   erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 39989a97a4..5d4af7d0c8 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -547,10 +547,10 @@ theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
 theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+@[simp, grind =] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp, grind] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
+@[simp, grind =] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
     (a :: l).contains b = (b == a || l.contains b) := by
   simp only [contains, elem_cons]
   split <;> simp_all
@@ -624,10 +624,10 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
 /-! ### set -/
 
 -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
-@[simp, grind] theorem set_nil {i : Nat} {a : α} : [].set i a = [] := rfl
-@[simp, grind] theorem set_cons_zero {x : α} {xs : List α} {a : α} :
+@[simp, grind =] theorem set_nil {i : Nat} {a : α} : [].set i a = [] := rfl
+@[simp, grind =] theorem set_cons_zero {x : α} {xs : List α} {a : α} :
   (x :: xs).set 0 a = a :: xs := rfl
-@[simp, grind] theorem set_cons_succ {x : α} {xs : List α} {i : Nat} {a : α} :
+@[simp, grind =] theorem set_cons_succ {x : α} {xs : List α} {i : Nat} {a : α} :
   (x :: xs).set (i + 1) a = x :: xs.set i a := rfl
 
 @[simp] theorem getElem_set_self {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
@@ -747,10 +747,10 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.s
 
 /-! ### BEq -/
 
-@[simp, grind] theorem beq_nil_eq [BEq α] {l : List α} : (l == []) = l.isEmpty := by
+@[simp, grind =] theorem beq_nil_eq [BEq α] {l : List α} : (l == []) = l.isEmpty := by
   cases l <;> rfl
 
-@[simp, grind] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
+@[simp, grind =] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
   cases l <;> rfl
 
 @[deprecated beq_nil_eq (since := "2025-04-04")]
@@ -759,7 +759,7 @@ abbrev beq_nil_iff := @beq_nil_eq
 @[deprecated nil_beq_eq (since := "2025-04-04")]
 abbrev nil_beq_iff := @nil_beq_eq
 
-@[simp, grind] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
+@[simp, grind =] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
     (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
 
 @[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
@@ -839,7 +839,7 @@ theorem getElem_length_sub_one_eq_getLast {l : List α} (h : l.length - 1 < l.le
     l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
   rw [← getLast_eq_getElem]
 
-@[simp, grind] theorem getLast_cons_cons {a : α} {l : List α} :
+@[simp, grind =] theorem getLast_cons_cons {a : α} {l : List α} :
     getLast (a :: b :: l) (by simp) = getLast (b :: l) (by simp) :=
   rfl
 
@@ -852,10 +852,10 @@ theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil),
 theorem getLast_eq_getLastD {a l} (h) : @getLast α (a::l) h = getLastD l a := by
   cases l <;> rfl
 
-@[simp, grind] theorem getLastD_eq_getLast? {a l} : @getLastD α l a = (getLast? l).getD a := by
+@[simp, grind =] theorem getLastD_eq_getLast? {a l} : @getLastD α l a = (getLast? l).getD a := by
   cases l <;> rfl
 
-@[simp, grind] theorem getLast_singleton {a} (h) : @getLast α [a] h = a := rfl
+@[simp, grind =] theorem getLast_singleton {a} (h) : @getLast α [a] h = a := rfl
 
 theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
@@ -1017,18 +1017,18 @@ theorem head_of_mem_head? {l : List α} {x} (hx : x ∈ l.head?) :
 /-! ### headD -/
 
 /-- `simp` unfolds `headD` in terms of `head?` and `Option.getD`. -/
-@[simp, grind] theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a := by
+@[simp, grind =] theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a := by
   cases l <;> simp [headD]
 
 /-! ### tailD -/
 
 /-- `simp` unfolds `tailD` in terms of `tail?` and `Option.getD`. -/
-@[simp, grind] theorem tailD_eq_tail? {l l' : List α} : tailD l l' = (tail? l).getD l' := by
+@[simp, grind =] theorem tailD_eq_tail? {l l' : List α} : tailD l l' = (tail? l).getD l' := by
   cases l <;> rfl
 
 /-! ### tail -/
 
-@[simp, grind] theorem length_tail {l : List α} : l.tail.length = l.length - 1 := by cases l <;> rfl
+@[simp, grind =] theorem length_tail {l : List α} : l.tail.length = l.length - 1 := by cases l <;> rfl
 
 theorem tail_eq_tailD {l : List α} : l.tail = tailD l [] := by cases l <;> rfl
 
@@ -1040,13 +1040,13 @@ theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := b
 theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ [] := by
   cases l <;> simp
 
-@[simp, grind] theorem getElem_tail {l : List α} {i : Nat} (h : i < l.tail.length) :
+@[simp, grind =] theorem getElem_tail {l : List α} {i : Nat} (h : i < l.tail.length) :
     (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by
   cases l with
   | nil => simp at h
   | cons _ l => simp
 
-@[simp, grind] theorem getElem?_tail {l : List α} {i : Nat} :
+@[simp, grind =] theorem getElem?_tail {l : List α} {i : Nat} :
     (tail l)[i]? = l[i + 1]? := by
   cases l <;> simp
 
@@ -1070,7 +1070,7 @@ theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.l
 @[simp] theorem head?_tail {l : List α} : (tail l).head? = l[1]? := by
   simp [head?_eq_getElem?]
 
-@[simp, grind] theorem getLast_tail {l : List α} (h : l.tail ≠ []) :
+@[simp, grind =] theorem getLast_tail {l : List α} (h : l.tail ≠ []) :
     (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by
   simp only [getLast_eq_getElem, length_tail, getElem_tail]
   congr
@@ -1096,7 +1096,7 @@ theorem cons_head_tail (h : l ≠ []) : l.head h :: l.tail = l := by
 
 /-! ### map -/
 
-@[simp, grind] theorem length_map {as : List α} (f : α → β) : (as.map f).length = as.length := by
+@[simp, grind =] theorem length_map {as : List α} (f : α → β) : (as.map f).length = as.length := by
   induction as with
   | nil => simp [List.map]
   | cons _ as ih => simp [List.map, ih]
@@ -1104,13 +1104,13 @@ theorem cons_head_tail (h : l ≠ []) : l.head h :: l.tail = l := by
 @[simp] theorem isEmpty_map {l : List α} {f : α → β} : (l.map f).isEmpty = l.isEmpty := by
   cases l <;> simp
 
-@[simp, grind] theorem getElem?_map {f : α → β} : ∀ {l : List α} {i : Nat}, (map f l)[i]? = Option.map f l[i]?
+@[simp, grind =] theorem getElem?_map {f : α → β} : ∀ {l : List α} {i : Nat}, (map f l)[i]? = Option.map f l[i]?
   | [], _ => rfl
   | _ :: _, 0 => by simp
   | _ :: l, i+1 => by simp [getElem?_map]
 
 -- The argument `f : α → β` is explicit, to facilitate rewriting from right to left.
-@[simp, grind] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
+@[simp, grind =] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
     (map f l)[i] = f (l[i]'(length_map f ▸ h)) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
 
@@ -1315,7 +1315,7 @@ theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀
 @[deprecated length_filter_eq_length_iff (since := "2025-04-04")]
 abbrev filter_length_eq_length := @length_filter_eq_length_iff
 
-@[simp, grind] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
+@[simp, grind =] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
   induction as with
   | nil => simp
   | cons a as ih =>
@@ -1377,7 +1377,7 @@ theorem map_filter_eq_foldr {f : α → β} {p : α → Bool} {as : List α} :
     simp only [foldr]
     cases hp : p head <;> simp [filter, *]
 
-@[simp, grind] theorem filter_append {p : α → Bool} :
+@[simp, grind =] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], _ => rfl
   | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
@@ -1442,7 +1442,7 @@ theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
   erw [filterMap_eq_map]
   simp
 
-@[simp, grind] theorem filterMap_some {l : List α} : filterMap some l = l := by
+@[simp, grind =] theorem filterMap_some {l : List α} : filterMap some l = l := by
   rw [filterMap_some_fun, id]
 
 theorem map_filterMap_some_eq_filter_map_isSome {f : α → Option β} {l : List α} :
@@ -1489,7 +1489,7 @@ theorem map_filterMap {f : α → Option β} {g : β → γ} {l : List α} :
     map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
   simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]
 
-@[simp, grind]
+@[simp, grind =]
 theorem filterMap_map {f : α → β} {g : β → Option γ} {l : List α} :
     filterMap g (map f l) = filterMap (g ∘ f) l := by
   rw [← filterMap_eq_map, filterMap_filterMap]; rfl
@@ -1504,7 +1504,7 @@ theorem filterMap_filter {p : α → Bool} {f : α → Option β} {l : List α}
   rw [← filterMap_eq_filter, filterMap_filterMap]
   congr; funext x; by_cases h : p x <;> simp [Option.guard, h]
 
-@[simp, grind] theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
+@[simp, grind =] theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   induction l <;> simp [filterMap_cons]; split <;> simp [*, eq_comm]
 
@@ -1516,7 +1516,7 @@ theorem forall_mem_filterMap {f : α → Option β} {l : List α} {P : β → Pr
   intro a
   rw [forall_comm]
 
-@[simp, grind] theorem filterMap_append {l l' : List α} {f : α → Option β} :
+@[simp, grind =] theorem filterMap_append {l l' : List α} {f : α → Option β} :
     filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
   induction l <;> simp [filterMap_cons]; split <;> simp [*]
 
@@ -1588,7 +1588,7 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 @[simp] theorem cons_append_fun {a : α} {as : List α} :
     (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
 
-@[simp, grind] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+@[simp, grind =] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   induction s <;> simp_all [or_assoc]
 
 theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
@@ -1738,7 +1738,7 @@ theorem append_eq_append_iff {ws xs ys zs : List α} :
   | nil => simp_all
   | cons a as ih => cases ys <;> simp [eq_comm, and_assoc, ih, and_or_left]
 
-@[simp, grind] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
+@[simp, grind =] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
     head (l ++ l') w₁ = head l w₂ := by
   match l, w₂ with
   | a :: l, _ => rfl
@@ -1764,7 +1764,7 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
     head (l₁ ++ l₂) w = head l₂ (by simp_all) := by
   rw [head_append, dif_pos (by simp_all)]
 
-@[simp, grind] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
+@[simp, grind =] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
   cases l <;> simp
 
 -- Note:
@@ -1843,7 +1843,7 @@ theorem append_eq_filter_iff {p : α → Bool} :
     L₁ ++ L₂ = filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by
   rw [eq_comm, filter_eq_append_iff]
 
-@[simp, grind] theorem map_append {f : α → β} : ∀ {l₁ l₂}, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
+@[simp, grind =] theorem map_append {f : α → β} : ∀ {l₁ l₂}, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
   intro l₁; induction l₁ <;> intros <;> simp_all
 
 theorem map_eq_append_iff {f : α → β} :
@@ -2091,7 +2091,7 @@ theorem length_flatMap {l : List α} {f : α → List β} :
     length (l.flatMap f) = sum (map (fun a => (f a).length) l) := by
   rw [List.flatMap, length_flatten, map_map, Function.comp_def]
 
-@[simp, grind] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+@[simp, grind =] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
@@ -2171,7 +2171,7 @@ theorem flatMap_eq_foldl {f : α → List β} {l : List α} :
 theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
   induction n <;> simp_all [replicate_succ, ← cons_append]
 
-@[simp, grind] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
+@[simp, grind =] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
   | 0 => by simp
   | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
 
@@ -2196,7 +2196,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 @[simp] theorem replicate_eq_nil_iff {n : Nat} (a : α) : replicate n a = [] ↔ n = 0 := by
   cases n <;> simp
 
-@[simp, grind] theorem getElem_replicate {a : α} {n : Nat} {i : Nat} (h : i < (replicate n a).length) :
+@[simp, grind =] theorem getElem_replicate {a : α} {n : Nat} {i : Nat} (h : i < (replicate n a).length) :
     (replicate n a)[i] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
@@ -2400,7 +2400,7 @@ termination_by l.length
 
 /-! ### reverse -/
 
-@[simp, grind] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by
+@[simp, grind =] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
@@ -2409,7 +2409,7 @@ theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈
   | [], _ => ⟨.inr, fun | .inr h => h⟩
   | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]
 
-@[simp, grind] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by
+@[simp, grind =] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by
   simp [reverse, mem_reverseAux]
 
 @[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by
@@ -2433,14 +2433,14 @@ theorem getElem?_reverse' : ∀ {l : List α} {i j}, i + j + 1 = length l →
     rw [getElem?_append_left, getElem?_reverse' this]
     rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
     l.reverse[i]? = l[l.length - 1 - i]? :=
   getElem?_reverse' <| by
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
     l.reverse[i] = l[l.length - 1 - i]'(Nat.sub_one_sub_lt_of_lt (by simpa using h)) := by
   apply Option.some.inj
@@ -2453,7 +2453,7 @@ theorem reverseAux_reverseAux_nil {as bs : List α} : reverseAux (reverseAux as
   | cons a as ih => simp [reverseAux, ih]
 
 -- The argument `as : List α` is explicit to allow rewriting from right to left.
-@[simp, grind] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
+@[simp, grind =] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
   simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl
 
 theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse := by
@@ -2466,10 +2466,10 @@ theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse :
     xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a] := by
   rw [reverse_eq_iff, reverse_cons]
 
-@[simp, grind] theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
+@[simp, grind =] theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
   cases l <;> simp [getLast?_concat]
 
-@[simp, grind] theorem head?_reverse {l : List α} : l.reverse.head? = l.getLast? := by
+@[simp, grind =] theorem head?_reverse {l : List α} : l.reverse.head? = l.getLast? := by
   rw [← getLast?_reverse, reverse_reverse]
 
 theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head? := by
@@ -2542,7 +2542,7 @@ theorem flatten_reverse {L : List (List α)} :
 @[simp] theorem reverseAux_eq {as bs : List α} : reverseAux as bs = reverse as ++ bs :=
   reverseAux_eq_append ..
 
-@[simp, grind] theorem reverse_replicate {n : Nat} {a : α} : (replicate n a).reverse = replicate n a :=
+@[simp, grind =] theorem reverse_replicate {n : Nat} {a : α} : (replicate n a).reverse = replicate n a :=
   eq_replicate_iff.2
     ⟨by rw [length_reverse, length_replicate],
      fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
@@ -2554,7 +2554,7 @@ theorem flatten_reverse {L : List (List α)} :
     (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
   induction l generalizing b <;> simp [*]
 
-@[simp, grind] theorem foldrM_cons [Monad m] [LawfulMonad m] {a : α} {l : List α} {f : α → β → m β} {b : β} :
+@[simp, grind =] theorem foldrM_cons [Monad m] [LawfulMonad m] {a : α} {l : List α} {f : α → β → m β} {b : β} :
     (a :: l).foldrM f b = l.foldrM f b >>= f a := by
   simp only [foldrM]
   induction l <;> simp_all
@@ -2598,15 +2598,19 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
 
 /-! ### foldl and foldr -/
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
+-- foldr_cons_eq_append: [@foldr #4 (List #3) _ #0 #2, @map _ _ #1 #2]
 @[simp, grind] theorem foldr_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
     l.foldr (fun x ys => f x :: ys) l' = l.map f ++ l' := by
   induction l <;> simp [*]
 
 /-- Variant of `foldr_cons_eq_append` specalized to `f = id`. -/
-@[simp, grind] theorem foldr_cons_eq_append' {l l' : List β} :
+@[simp, grind =] theorem foldr_cons_eq_append' {l l' : List β} :
     l.foldr cons l' = l ++ l' := by
   induction l <;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
+-- foldl_flip_cons_eq_append: [@foldl (List #3) #4 _ #0 #2, @map _ _ #1 #2]
 @[simp, grind] theorem foldl_flip_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
     l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
   induction l generalizing l' <;> simp [*]
@@ -2616,18 +2620,22 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
     l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
   simp
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
   induction l <;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
   induction l generalizing l'<;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldr_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (fun x ys => ys ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
   induction l generalizing l' <;> simp [*]
 
+-- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
 @[simp, grind] theorem foldl_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldl (fun xs y => f y ++ xs) l' = (l.map f).reverse.flatten ++ l' := by
   induction l generalizing l' <;> simp [*]
@@ -2690,11 +2698,11 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
     (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
   induction L <;> simp_all
 
-@[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
+@[simp, grind =] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
     l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by
   simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure]
 
-@[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
+@[simp, grind =] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
@@ -2848,7 +2856,7 @@ theorem foldr_rel {l : List α} {f : α → β → β} {g : α → γ → γ} {a
 
 /-! #### Further results about `getLast` and `getLast?` -/
 
-@[simp, grind] theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
+@[simp, grind =] theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.head h = getLast l (by simp_all) := by
   induction l with
   | nil => contradiction
@@ -2878,7 +2886,7 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   rw [getLast?_eq_head?_reverse, isSome_head?]
   simp
 
-@[simp, grind] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
+@[simp, grind =] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.getLast h = l.head (by simp_all) := by
   simp [getLast_eq_head_reverse]
 
@@ -2912,7 +2920,7 @@ theorem getLast_append_left {l : List α} (w : l ++ l' ≠ []) (h : l' = []) :
     (l ++ l').getLast w = l.getLast (by simp_all) := by
   rw [getLast_append, dif_pos (by simp_all)]
 
-@[simp, grind] theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast? := by
+@[simp, grind =] theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast? := by
   simp [← head?_reverse]
 
 theorem getLast_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (getLast l w) = true) :
@@ -2948,7 +2956,7 @@ theorem getLast?_replicate {a : α} {n : Nat} : (replicate n a).getLast? = if n
 /-! ### leftpad -/
 
 -- We unfold `leftpad` and `rightpad` for verification purposes.
-attribute [simp, grind] leftpad rightpad
+attribute [simp, grind =] leftpad rightpad
 
 -- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
@@ -2982,12 +2990,12 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_map [BEq β] {l : List α} {x : β} {f : α → β} :
     (l.map f).contains x = l.any (fun a => x == f a) := by
   induction l with simp_all
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_filter [BEq α] {l : List α} {x : α} {p : α → Bool} :
     (l.filter p).contains x = l.any (fun a => x == a && p a) := by
   induction l with
@@ -2996,7 +3004,7 @@ theorem contains_filter [BEq α] {l : List α} {x : α} {p : α → Bool} :
     simp only [filter_cons, any_cons]
     split <;> simp_all
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_filterMap [BEq β] {l : List α} {x : β} {f : α → Option β} :
     (l.filterMap f).contains x = l.any (fun a => (f a).any fun b => x == b) := by
   induction l with
@@ -3012,21 +3020,21 @@ theorem contains_append [BEq α] {l₁ l₂ : List α} {x : α} :
   | nil => simp
   | cons a l ih => simp [ih, Bool.or_assoc]
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatten [BEq α] {l : List (List α)} {x : α} :
     l.flatten.contains x = l.any fun l => l.contains x := by
   induction l with
   | nil => simp
   | cons _ l ih => simp [ih]
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_reverse [BEq α] {l : List α} {x : α} :
     (l.reverse).contains x = l.contains x := by
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, Bool.or_comm]
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatMap [BEq β] {l : List α} {f : α → List β} {x : β} :
     (l.flatMap f).contains x = l.any fun a => (f a).contains x := by
   induction l with
@@ -3041,7 +3049,7 @@ Because we immediately simplify `partition` into two `filter`s for verification
 we do not separately develop much theory about it.
 -/
 
-@[simp, grind] theorem partition_eq_filter_filter {p : α → Bool} {l : List α} :
+@[simp, grind =] theorem partition_eq_filter_filter {p : α → Bool} {l : List α} :
     partition p l = (filter p l, filter (not ∘ p) l) := by simp [partition, aux]
   where
     aux : ∀ l {as bs}, partition.loop p l (as, bs) =
@@ -3061,11 +3069,11 @@ grind_pattern mem_partition => a ∈ (partition p l).2
 are often used for theorems about `Array.pop`.
 -/
 
-@[simp, grind] theorem length_dropLast : ∀ {xs : List α}, xs.dropLast.length = xs.length - 1
+@[simp, grind =] theorem length_dropLast : ∀ {xs : List α}, xs.dropLast.length = xs.length - 1
   | [] => rfl
   | x::xs => by simp
 
-@[simp, grind] theorem getElem_dropLast : ∀ {xs : List α} {i : Nat} (h : i < xs.dropLast.length),
+@[simp, grind =] theorem getElem_dropLast : ∀ {xs : List α} {i : Nat} (h : i < xs.dropLast.length),
     xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _))
   | _ :: _ :: _, 0, _ => rfl
   | _ :: _ :: _, _ + 1, h => getElem_dropLast (Nat.add_one_lt_add_one_iff.mp h)
@@ -3268,24 +3276,24 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
   | nil => rfl
   | cons h t ih => simp_all [Bool.and_assoc]
 
-@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
+@[simp, grind =] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
   induction l <;> simp_all
 
-@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
+@[simp, grind =] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
   induction l <;> simp_all
 
-@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
+@[simp, grind =] theorem any_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).any p = l.any fun a => (f a).any p := by
   induction l <;> simp_all
 
-@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
+@[simp, grind =] theorem all_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).all p = l.all fun a => (f a).all p := by
   induction l <;> simp_all
 
-@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
+@[simp, grind =] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
   induction l <;> simp_all [Bool.or_comm]
 
-@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
+@[simp, grind =] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
   induction l <;> simp_all [Bool.and_comm]
 
 @[simp] theorem any_replicate {n : Nat} {a : α} :
@@ -3335,7 +3343,7 @@ variable [BEq α]
     simp only [replace_cons]
     split <;> simp_all
 
-@[simp, grind] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
+@[simp, grind =] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
   | nil => simp
   | cons x l ih =>
@@ -3429,9 +3437,9 @@ end replace
 section insert
 variable [BEq α]
 
-@[simp, grind] theorem insert_nil (a : α) : [].insert a = [a] := rfl
+@[simp, grind =] theorem insert_nil (a : α) : [].insert a = [a] := rfl
 
-@[simp, grind] theorem contains_insert [PartialEquivBEq α] {l : List α} {a : α} {x : α} :
+@[simp, grind =] theorem contains_insert [PartialEquivBEq α] {l : List α} {a : α} {x : α} :
     (l.insert a).contains x = (x == a || l.contains x) := by
   simp only [List.insert]
   split <;> rename_i h
@@ -3448,7 +3456,7 @@ variable [LawfulBEq α]
 @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
   simp [List.insert, h]
 
-@[simp, grind] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
+@[simp, grind =] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
   if h : b ∈ l then
     rw [insert_of_mem h]
     constructor; {apply Or.inr}
@@ -3550,7 +3558,7 @@ theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂)
     (l₁ ++ l₂).insert a = l₁.insert a ++ l₂ := by
   simp [insert_append, h]
 
-@[simp, grind] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
+@[simp, grind =] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
   cases n <;> simp_all
 
 @[simp] theorem insert_replicate_ne {a b : α} (h : !b == a) :
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index e506911d4b..22cc521575 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -248,7 +248,7 @@ theorem pairwise_le_range {n : Nat} : Pairwise (· ≤ ·) (range n) :=
 theorem nodup_range {n : Nat} : Nodup (range n) := by
   simp +decide only [range_eq_range', nodup_range']
 
-@[simp, grind] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
+@[simp, grind =] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
   simp [range_eq_range']
 
diff --git a/src/Init/Data/Option/Array.lean b/src/Init/Data/Option/Array.lean
index 17dcc1a06d..976831eb80 100644
--- a/src/Init/Data/Option/Array.lean
+++ b/src/Init/Data/Option/Array.lean
@@ -15,30 +15,30 @@ public section
 
 namespace Option
 
-@[simp, grind] theorem mem_toArray {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a := by
+@[simp, grind =] theorem mem_toArray {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a := by
   cases o <;> simp [eq_comm]
 
-@[simp, grind] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) :
+@[simp, grind =] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) :
     forIn' o.toArray b f = forIn' o b fun a m b => f a (by simpa using m) b := by
   cases o <;> simp <;> rfl
 
-@[simp, grind] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
+@[simp, grind =] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn o.toArray b f = forIn o b f := by
   cases o <;> simp <;> rfl
 
-@[simp, grind] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
+@[simp, grind =] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
     o.toArray.foldlM f a = o.elim (pure a) (fun b => f a b) := by
   cases o <;> simp
 
-@[simp, grind] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
+@[simp, grind =] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
     o.toArray.foldrM f a = o.elim (pure a) (fun b => f b a) := by
   cases o <;> simp
 
-@[simp, grind] theorem foldl_toArray (o : Option β) (a : α) (f : α → β → α) :
+@[simp, grind =] theorem foldl_toArray (o : Option β) (a : α) (f : α → β → α) :
     o.toArray.foldl f a = o.elim a (fun b => f a b) := by
   cases o <;> simp
 
-@[simp, grind] theorem foldr_toArray (o : Option β) (a : α) (f : β → α → α) :
+@[simp, grind =] theorem foldr_toArray (o : Option β) (a : α) (f : β → α → α) :
     o.toArray.foldr f a = o.elim a (fun b => f b a) := by
   cases o <;> simp
 
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index e95b959863..0e8cebeab3 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -18,27 +18,27 @@ 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 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 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
+@[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
   | none   => false
 
-@[simp, grind] theorem isSome_none : @isSome α none = false := rfl
-@[simp, grind] theorem isSome_some : isSome (some a) = true := rfl
+@[simp, grind =] theorem isSome_none : @isSome α none = false := rfl
+@[simp, grind =] theorem isSome_some : isSome (some a) = true := rfl
 
 /--
 Returns `true` on `none` and `false` on `some x`.
@@ -53,8 +53,8 @@ Examples:
   | some _ => false
   | none   => true
 
-@[simp, grind] theorem isNone_none : @isNone α none = true := rfl
-@[simp, grind] theorem isNone_some : isNone (some a) = false := rfl
+@[simp, grind =] theorem isNone_none : @isNone α none = true := rfl
+@[simp, grind =] theorem isNone_some : isNone (some a) = false := rfl
 
 /--
 Checks whether an optional value is both present and equal to some other value.
@@ -89,8 +89,8 @@ 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
+@[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
@@ -125,8 +125,8 @@ 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
+@[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
@@ -138,9 +138,9 @@ This is an alias for `Option.mapM`, which already works for applicative functors
   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 mapA_eq_mapM [Applicative m] {f : α → m β} : Option.mapA f o = Option.mapM f o := rfl
 
-@[simp, grind]
+@[simp, grind =]
 theorem map_id : (Option.map id : Option α → Option α) = id :=
   funext (fun o => match o with | none => rfl | some _ => rfl)
 
@@ -182,8 +182,8 @@ 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
+@[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.
@@ -197,8 +197,8 @@ 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
+@[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
@@ -210,8 +210,8 @@ 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
+@[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
@@ -351,9 +351,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, grind] 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, grind] 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.
@@ -431,8 +431,8 @@ Examples:
 -/
 @[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
+@[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.
@@ -457,8 +457,8 @@ some "world"
   | none => pure none
   | 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 α) : (some f).sequence = some <$> f := rfl
+@[simp, grind =] theorem sequence_none [Applicative m] : (none : Option (m α)).sequence = pure none := rfl
+@[simp, grind =] theorem sequence_some [Applicative m] (f : m α) : (some f).sequence = some <$> f := rfl
 
 /--
 A monadic case analysis function for `Option`.
@@ -483,8 +483,8 @@ 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
+@[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} := private
@@ -520,10 +520,10 @@ protected def min [Min α] : Option α → Option α → Option α
 
 instance [Min α] : Min (Option α) where min := Option.min
 
-@[simp, grind] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
-@[simp, grind] theorem min_none_left [Min α] {o : Option α} : min none o = none := by
+@[simp, grind =] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
+@[simp, grind =] theorem min_none_left [Min α] {o : Option α} : min none o = none := by
   cases o <;> rfl
-@[simp, grind] theorem min_none_right [Min α] {o : Option α} : min o none = none := by
+@[simp, grind =] theorem min_none_right [Min α] {o : Option α} : min o none = none := by
   cases o <;> rfl
 
 @[deprecated min_none_right (since := "2025-05-12")]
@@ -553,10 +553,10 @@ protected def max [Max α] : Option α → Option α → Option α
 
 instance [Max α] : Max (Option α) where max := Option.max
 
-@[simp, grind] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl
-@[simp, grind] theorem max_none_left [Max α] {o : Option α} : max none o = o := by
+@[simp, grind =] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl
+@[simp, grind =] theorem max_none_left [Max α] {o : Option α} : max none o = o := by
   cases o <;> rfl
-@[simp, grind] theorem max_none_right [Max α] {o : Option α} : max o none = o := by
+@[simp, grind =] theorem max_none_right [Max α] {o : Option α} : max o none = o := by
   cases o <;> rfl
 
 @[deprecated max_none_right (since := "2025-05-12")]
diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean
index 5a00b5b7ae..8b68dc7409 100644
--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -16,30 +16,30 @@ public section
 
 namespace Option
 
-@[simp, grind] 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, grind] 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, grind] 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, grind] 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, grind] 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, grind] 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, grind] 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
 
@@ -47,7 +47,7 @@ namespace Option
 theorem pairwise_toList {P : α → α → Prop} {o : Option α} : o.toList.Pairwise P := by
   cases o <;> simp
 
-@[simp, grind]
+@[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 8672a1c3a1..33bc73305c 100644
--- a/src/Init/Data/Option/Monadic.lean
+++ b/src/Init/Data/Option/Monadic.lean
@@ -16,20 +16,20 @@ public section
 
 namespace Option
 
-@[simp, grind] theorem bindM_none [Pure m] (f : α → m (Option β)) : none.bindM f = pure none := rfl
-@[simp, grind] theorem bindM_some [Pure m] (a) (f : α → m (Option β)) : (some a).bindM f = f a := by
+@[simp, grind =] theorem bindM_none [Pure m] (f : α → m (Option β)) : none.bindM f = pure none := rfl
+@[simp, grind =] theorem bindM_some [Pure m] (a) (f : α → m (Option β)) : (some a).bindM f = f a := by
   simp [Option.bindM]
 
 -- We simplify `Option.forM` to `forM`.
 @[simp] theorem forM_eq_forM [Monad m] : @Option.forM m α _ = forM := rfl
 
-@[simp, grind] theorem forM_none [Monad m] (f : α → m PUnit) :
+@[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 : α) :
+@[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) :
+@[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
 
@@ -37,11 +37,11 @@ theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α →
     forM o.join f = forM o (forM · f) := by
   cases o <;> simp
 
-@[simp, grind] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
+@[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 β)) :
+@[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]
@@ -49,11 +49,11 @@ theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α →
   funext x
   split <;> simp
 
-@[simp, grind] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
+@[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 β)) :
+@[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]
@@ -106,7 +106,7 @@ theorem forIn'_id_yield_eq_pelim
       o.pelim b (fun a h => f a h b) :=
   forIn'_pure_yield_eq_pelim _ _ _
 
-@[simp, grind] 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
@@ -149,7 +149,7 @@ theorem forIn_id_yield_eq_elim
       o.elim b (fun a => f a b) :=
   forIn_pure_yield_eq_elim _ _ _
 
-@[simp, grind] 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
diff --git a/src/Init/Data/Order/Ord.lean b/src/Init/Data/Order/Ord.lean
index a6fcc421da..26a48e876d 100644
--- a/src/Init/Data/Order/Ord.lean
+++ b/src/Init/Data/Order/Ord.lean
@@ -349,7 +349,7 @@ theorem LawfulEqCmp.compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b :=
   beq_iff_eq.trans compare_eq_iff_eq
 
 /-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_eq_iff_eq` -/
-@[simp, grind]
+@[simp, grind =]
 theorem LawfulEqOrd.compare_eq_iff_eq [Ord α] [LawfulEqOrd α] {a b : α} :
     compare a b = .eq ↔ a = b :=
   LawfulEqCmp.compare_eq_iff_eq
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 13154481d2..570be2b693 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -200,7 +200,7 @@ theorem mem_attach (xs : Vector α n) : ∀ x, x ∈ xs.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
-@[simp, grind]
+@[simp, grind =]
 theorem mem_attachWith {xs : Vector α n} {q : α → Prop} (H) (x : {x // q x}) :
     x ∈ xs.attachWith q H ↔ x.1 ∈ xs := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index f7e90ba3c8..1aafed6f59 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -36,7 +36,7 @@ structure Vector (α : Type u) (n : Nat) where
   size_toArray : toArray.size = n
 deriving Repr, DecidableEq
 
-attribute [simp, grind] Vector.size_toArray
+attribute [simp, grind =] Vector.size_toArray
 
 /--
 Converts an array to a vector. The resulting vector's size is the array's size.
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
index 3338b64b27..44d2170040 100644
--- a/src/Init/Data/Vector/Find.lean
+++ b/src/Init/Data/Vector/Find.lean
@@ -32,8 +32,8 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp, grind] theorem findSome?_empty : (#v[] : Vector α 0).findSome? f = none := rfl
-@[simp, grind] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind =] theorem findSome?_empty : (#v[] : Vector α 0).findSome? f = none := rfl
+@[simp, grind =] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp
 
 @[grind]
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 7226389ed1..230a6e945d 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -266,12 +266,12 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 
 /-! ### toArray lemmas -/
 
-@[simp, grind] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) :
+@[simp, grind =] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := by
   cases xs
   simp
 
-@[simp, grind] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} :
+@[simp, grind =] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} :
     xs.toArray[i]? = xs[i]? := by
   cases xs
   simp
@@ -280,45 +280,45 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
     (xs ++ ys).toArray = xs.toArray ++ ys.toArray := rfl
 
 set_option linter.indexVariables false in
-@[simp, grind] theorem toArray_drop {xs : Vector α n} {i} :
+@[simp, grind =] theorem toArray_drop {xs : Vector α n} {i} :
     (xs.drop i).toArray = xs.toArray.extract i n := by
   simp [drop]
 
 @[simp, grind =] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
-@[simp, grind] theorem toArray_emptyWithCapacity {cap} :
+@[simp, grind =] theorem toArray_emptyWithCapacity {cap} :
     (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
 
 @[deprecated toArray_emptyWithCapacity (since := "2025-03-12")]
 abbrev toArray_mkEmpty := @toArray_emptyWithCapacity
 
-@[simp, grind] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) :
+@[simp, grind =] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) :
     (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl
 
-@[simp, grind] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) :
+@[simp, grind =] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) :
     (xs.eraseIdx! i).toArray = xs.toArray.eraseIdx! i := by
   cases xs; simp_all [Array.eraseIdx!]
 
-@[simp, grind] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) :
+@[simp, grind =] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) :
     (xs.insertIdx i x h).toArray = xs.toArray.insertIdx i x (by simp [h]) := rfl
 
-@[simp, grind] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) :
+@[simp, grind =] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) :
     (xs.insertIdx! i x).toArray = xs.toArray.insertIdx! i x := by
   cases xs; simp_all [Array.insertIdx!]
 
-@[simp, grind] theorem toArray_cast {xs : Vector α n} (h : n = m) :
+@[simp, grind =] theorem toArray_cast {xs : Vector α n} (h : n = m) :
     (xs.cast h).toArray = xs.toArray := rfl
 
-@[simp, grind] theorem toArray_extract {xs : Vector α n} {start stop} :
+@[simp, grind =] theorem toArray_extract {xs : Vector α n} {start stop} :
     (xs.extract start stop).toArray = xs.toArray.extract start stop := rfl
 
-@[simp, grind] theorem toArray_map {f : α → β} {xs : Vector α n} :
+@[simp, grind =] theorem toArray_map {f : α → β} {xs : Vector α n} :
     (xs.map f).toArray = xs.toArray.map f := rfl
 
-@[simp, grind] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} :
+@[simp, grind =] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} :
     (xs.mapIdx f).toArray = xs.toArray.mapIdx f := rfl
 
-@[simp, grind] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} :
+@[simp, grind =] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} :
     (xs.mapFinIdx f).toArray =
       xs.toArray.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)) :=
   rfl
@@ -336,42 +336,42 @@ private theorem toArray_mapM_go [Monad m] [LawfulMonad m] {f : α → m β} {xs
     rfl
   · simp
 
-@[simp, grind] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} :
+@[simp, grind =] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} :
     toArray <$> xs.mapM f = xs.toArray.mapM f := by
   rcases xs with ⟨xs, rfl⟩
   unfold mapM
   rw [toArray_mapM_go]
   rfl
 
-@[simp, grind] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl
+@[simp, grind =] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl
 
-@[simp, grind] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl
+@[simp, grind =] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl
 
-@[simp, grind] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl
+@[simp, grind =] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl
 
-@[simp, grind] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} :
+@[simp, grind =] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} :
     (xs.toArray == ys.toArray) = (xs == ys) := by
   simp [instBEq, isEqv, Array.instBEq, Array.isEqv, xs.2, ys.2]
 
-@[simp, grind] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
+@[simp, grind =] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
 
-@[simp, grind] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl
+@[simp, grind =] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl
 
-@[simp, grind] theorem toArray_set {xs : Vector α n} {i x} (h) :
+@[simp, grind =] theorem toArray_set {xs : Vector α n} {i x} (h) :
     (xs.set i x).toArray = xs.toArray.set i x (by simpa using h):= rfl
 
-@[simp, grind] theorem toArray_set! {xs : Vector α n} {i x} :
+@[simp, grind =] theorem toArray_set! {xs : Vector α n} {i x} :
     (xs.set! i x).toArray = xs.toArray.set! i x := rfl
 
-@[simp, grind] theorem toArray_setIfInBounds {xs : Vector α n} {i x} :
+@[simp, grind =] theorem toArray_setIfInBounds {xs : Vector α n} {i x} :
     (xs.setIfInBounds i x).toArray = xs.toArray.setIfInBounds i x := rfl
 
-@[simp, grind] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl
+@[simp, grind =] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl
 
-@[simp, grind] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray =
+@[simp, grind =] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray =
     xs.toArray.swap i j (by simp [hj]) (by simp [hi]) := rfl
 
-@[simp, grind] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} :
+@[simp, grind =] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} :
     (xs.swapIfInBounds i j).toArray = xs.toArray.swapIfInBounds i j := rfl
 
 theorem toArray_swapAt {xs : Vector α n} {i x} (h) :
@@ -383,98 +383,98 @@ theorem toArray_swapAt! {xs : Vector α n} {i x} :
     ((xs.swapAt! i x).fst, (xs.swapAt! i x).snd.toArray) =
       ((xs.toArray.swapAt! i x).fst, (xs.toArray.swapAt! i x).snd) := rfl
 
-@[simp, grind] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl
+@[simp, grind =] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl
 
-@[simp, grind] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) :
+@[simp, grind =] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) :
     (xs.zipIdx k).toArray = xs.toArray.zipIdx k := rfl
 
-@[simp, grind] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
+@[simp, grind =] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
     (Vector.zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray := rfl
 
-@[simp, grind] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind =] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.anyM p = xs.anyM p := by
   cases xs
   simp
 
-@[simp, grind] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind =] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.allM p = xs.allM p := by
   cases xs
   simp
 
-@[simp, grind] theorem any_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem any_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.any p = xs.any p := by
   cases xs
   simp
 
-@[simp, grind] theorem all_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem all_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.all p = xs.all p := by
   cases xs
   simp
 
-@[simp, grind] theorem countP_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem countP_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.countP p = xs.countP p := by
   cases xs
   simp
 
-@[simp, grind] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} :
+@[simp, grind =] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} :
     xs.toArray.count a = xs.count a := by
   cases xs
   simp
 
-@[simp, grind] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} :
+@[simp, grind =] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} :
     xs.toArray.replace a b = (xs.replace a b).toArray := rfl
 
-@[simp, grind] theorem find?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem find?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.find? p = xs.find? p := by
   cases xs
   simp
 
-@[simp, grind] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} :
+@[simp, grind =] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} :
     xs.toArray.findSome? f = xs.findSome? f := by
   cases xs
   simp
 
-@[simp, grind] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.findRev? p = xs.findRev? p := by
   cases xs
   simp
 
-@[simp, grind] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} :
+@[simp, grind =] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} :
     xs.toArray.findSomeRev? f = xs.findSomeRev? f := by
   cases xs
   simp
 
-@[simp, grind] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind =] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.findM? p = xs.findM? p := by
   cases xs
   simp
 
-@[simp, grind] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
+@[simp, grind =] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
     xs.toArray.findSomeM? f = xs.findSomeM? f := by
   cases xs
   simp
 
-@[simp, grind] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind =] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.findRevM? p = xs.findRevM? p := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
+@[simp, grind =] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
     xs.toArray.findSomeRevM? f = xs.findSomeRevM? f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} :
+@[simp, grind =] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} :
     xs.toArray.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast xs.size_toArray.symm) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind =] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast xs.size_toArray.symm) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
+@[simp, grind =] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
 
 @[deprecated toArray_replicate (since := "2025-03-18")]
 abbrev toArray_mkVector := @toArray_replicate
@@ -503,13 +503,13 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
 
 /-! ### toList -/
 
-@[simp, grind] theorem length_toList {xs : Vector α n} : xs.toList.length = n := by
+@[simp, grind =] theorem length_toList {xs : Vector α n} : xs.toList.length = n := by
   rcases xs with ⟨xs, rfl⟩
   simp [toList]
 
 @[grind =_] theorem toList_toArray {xs : Vector α n} : xs.toArray.toList = xs.toList := rfl
 
-@[simp, grind] theorem toList_mk : (Vector.mk xs h).toList = xs.toList := rfl
+@[simp, grind =] theorem toList_mk : (Vector.mk xs h).toList = xs.toList := rfl
 
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
@@ -784,7 +784,7 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
 
 /-! ### replicate -/
 
-@[simp, grind] theorem replicate_zero : replicate 0 a = #v[] := rfl
+@[simp, grind =] theorem replicate_zero : replicate 0 a = #v[] := rfl
 
 @[deprecated replicate_zero (since := "2025-03-18")]
 abbrev replicate_mkVector := @replicate_zero
@@ -1215,7 +1215,7 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈
 
 @[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
 
-@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+@[simp, grind =] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
   rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]
 
@@ -1294,7 +1294,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 
 /-! ### setIfInBounds -/
 
-@[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
+@[simp, grind =] theorem setIfInBounds_empty {i : Nat} {a : α} :
     #v[].setIfInBounds i a = #v[] := rfl
 
 @[grind] theorem getElem_setIfInBounds {xs : Vector α n} {x : α} (hj : j < n) :
@@ -1347,7 +1347,7 @@ theorem mem_setIfInBounds {xs : Vector α n} {a : α} (hi : i < n) :
 
 /-! ### BEq -/
 
-@[simp, grind] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {xs : Vector α n} {ys : Vector α n} :
+@[simp, grind =] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {xs : Vector α n} {ys : Vector α n} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
   cases ys
@@ -1430,12 +1430,12 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by
 /-! ### map -/
 
 -- The argument `f : α → β` is explicit, to facilitate rewriting from right to left.
-@[simp, grind] theorem getElem_map (f : α → β) {xs : Vector α n} (hi : i < n) :
+@[simp, grind =] theorem getElem_map (f : α → β) {xs : Vector α n} (hi : i < n) :
     (xs.map f)[i] = f xs[i] := by
   cases xs
   simp
 
-@[simp, grind] theorem getElem?_map {f : α → β} {xs : Vector α n} {i : Nat}:
+@[simp, grind =] theorem getElem?_map {f : α → β} {xs : Vector α n} {i : Nat}:
     (xs.map f)[i]? = xs[i]?.map f := by
   cases xs
   simp
@@ -1445,7 +1445,7 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by
 theorem map_empty {f : α → β} : map f #v[] = #v[] := by
   simp
 
-@[simp, grind] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
+@[simp, grind =] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
   cases as
   simp
@@ -1620,7 +1620,7 @@ theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
 
 theorem singleton_eq_toVector_singleton {a : α} : #v[a] = #[a].toVector := rfl
 
-@[simp, grind] theorem mem_append {a : α} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem mem_append {a : α} {xs : Vector α n} {ys : Vector α m} :
     a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys := by
   cases xs
   cases ys
@@ -1656,12 +1656,12 @@ theorem forall_mem_append {p : α → Prop} {xs : Vector α n} {ys : Vector α m
     (∀ (x) (_ : x ∈ xs ++ ys), p x) ↔ (∀ (x) (_ : x ∈ xs), p x) ∧ (∀ (x) (_ : x ∈ ys), p x) := by
   simp only [mem_append, or_imp, forall_and]
 
-@[simp, grind]
+@[simp, grind =]
 theorem empty_append {xs : Vector α n} : (#v[] : Vector α 0) ++ xs = xs.cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem append_empty {xs : Vector α n} : xs ++ (#v[] : Vector α 0) = xs := by
   rw [← toArray_inj, toArray_append, Array.append_empty]
 
@@ -1771,7 +1771,7 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
       right
       refine ⟨cs.toArray, ha, rfl⟩
 
-@[simp, grind] theorem append_assoc {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} :
+@[simp, grind =] theorem append_assoc {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} :
     (xs ++ ys) ++ zs = (xs ++ (ys ++ zs)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -1826,7 +1826,7 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
     (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - n) x := by
   rw [setIfInBounds_append, if_neg (by omega)]
 
-@[simp, grind] theorem map_append {f : α → β} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem map_append {f : α → β} {xs : Vector α n} {ys : Vector α m} :
     map f (xs ++ ys) = map f xs ++ map f ys := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -1895,7 +1895,7 @@ theorem getElem?_flatten {xss : Vector (Vector β m) n} {i : Nat} :
         none := by
   simp [getElem?_def]
 
-@[simp, grind] theorem flatten_singleton {xs : Vector α n} : #v[xs].flatten = xs.cast (by simp) := by
+@[simp, grind =] theorem flatten_singleton {xs : Vector α n} : #v[xs].flatten = xs.cast (by simp) := by
   simp [flatten]
 
 set_option linter.listVariables false in
@@ -1922,7 +1922,7 @@ theorem forall_mem_flatten {p : α → Prop} {xss : Vector (Vector α n) m} :
   induction xss using vector₂_induction with
   | of xss h₁ h₂ => simp
 
-@[simp, grind] theorem flatten_append {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
+@[simp, grind =] theorem flatten_append {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
     flatten (xss₁ ++ xss₂) = (flatten xss₁ ++ flatten xss₂).cast (by simp [Nat.add_mul]) := by
   induction xss₁ using vector₂_induction
   induction xss₂ using vector₂_induction
@@ -1982,10 +1982,10 @@ theorem flatMap_def {xs : Vector α n} {f : α → Vector β m} : xs.flatMap f =
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_def, Function.comp_def]
 
-@[simp, grind] theorem flatMap_empty {f : α → Vector β m} :
+@[simp, grind =] theorem flatMap_empty {f : α → Vector β m} :
     (#v[] : Vector α 0).flatMap f = #v[].cast (by simp) := rfl
 
-@[simp, grind] theorem flatMap_push {xs : Vector α n} {x : α} {f : α → Vector β m} :
+@[simp, grind =] theorem flatMap_push {xs : Vector α n} {x : α} {f : α → Vector β m} :
     (xs.push x).flatMap f = (xs.flatMap f ++ f x).cast (by simp [Nat.add_mul]) := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2011,7 +2011,7 @@ theorem getElem?_flatMap {xs : Vector α n} {f : α → Vector β m} {i : Nat} :
 
 @[simp] theorem flatMap_id' {xss : Vector (Vector α m) n} : xss.flatMap (fun xs => xs) = xss.flatten := by simp [flatMap_def]
 
-@[simp, grind] theorem mem_flatMap {f : α → Vector β m} {b} {xs : Vector α n} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
+@[simp, grind =] theorem mem_flatMap {f : α → Vector β m} {b} {xs : Vector α n} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
@@ -2074,7 +2074,7 @@ theorem replicate_succ' : replicate (n + 1) a = (#v[a] ++ replicate n a).cast (b
 @[deprecated replicate_succ' (since := "2025-03-18")]
 abbrev mkVector_succ' := @replicate_succ'
 
-@[simp, grind] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+@[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
   simp only [mem_mk]
   simp
@@ -2094,7 +2094,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 @[deprecated forall_mem_replicate (since := "2025-03-18")]
 abbrev forall_mem_mkVector := @forall_mem_replicate
 
-@[simp, grind] theorem getElem_replicate {a : α} (h : i < n) : (replicate n a)[i] = a := by
+@[simp, grind =] theorem getElem_replicate {a : α} (h : i < n) : (replicate n a)[i] = a := by
   rw [replicate_eq_mk_replicate, getElem_mk]
   simp
 
@@ -2227,16 +2227,16 @@ abbrev sum_mkVector := @sum_replicate_nat
 
 theorem reverse_empty : reverse (#v[] : Vector α 0) = #v[] := rfl
 
-@[simp, grind] theorem reverse_push {as : Vector α n} {a : α} :
+@[simp, grind =] theorem reverse_push {as : Vector α n} {a : α} :
     (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by
   rcases as with ⟨as, rfl⟩
   simp [Array.reverse_push]
 
-@[simp, grind] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
+@[simp, grind =] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
   cases as
   simp
 
-@[simp, grind] theorem getElem_reverse {xs : Vector α n} {i : Nat} (hi : i < n) :
+@[simp, grind =] theorem getElem_reverse {xs : Vector α n} {i : Nat} (hi : i < n) :
     (xs.reverse)[i] = xs[n - 1 - i] := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2252,14 +2252,14 @@ theorem getElem?_reverse' {xs : Vector α n} {i j : Nat} (h : i + j + 1 = n) : x
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.getElem?_reverse' h
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem?_reverse {xs : Vector α n} {i} (h : i < n) :
     xs.reverse[i]? = xs[n - 1 - i]? := by
   cases xs
   simp_all
 
 -- The argument `xs : Vector α n` is explicit so we can rewrite from right to left.
-@[simp, grind] theorem reverse_reverse (xs : Vector α n) : xs.reverse.reverse = xs := by
+@[simp, grind =] theorem reverse_reverse (xs : Vector α n) : xs.reverse.reverse = xs := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.reverse_reverse]
 
@@ -2279,7 +2279,7 @@ theorem reverse_eq_iff {xs ys : Vector α n} : xs.reverse = ys ↔ xs = ys.rever
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_reverse]
 
-@[simp, grind] theorem reverse_append {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem reverse_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).reverse = (ys.reverse ++ xs.reverse).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -2320,7 +2320,7 @@ theorem flatMap_reverse {xs : Vector α n} {f : α → Vector β m} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_reverse, Function.comp_def]
 
-@[simp, grind] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
+@[simp, grind =] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
   rw [← toArray_inj]
   simp
 
@@ -2365,7 +2365,7 @@ theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} :
     foldrM f init #v[] = return init := by
   simp
 
-@[simp, grind] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} :
+@[simp, grind =] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} :
     (xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2410,7 +2410,7 @@ theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Vector α n} {a : α} :
+@[simp, grind =] theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Vector α n} {a : α} :
     (xs.push a).foldrM f init = f a init >>= xs.foldrM f := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2433,12 +2433,12 @@ theorem foldr_congr {xs ys : Vector α n} (h₀ : xs = ys) {f g : α → β →
     xs.foldr f a = ys.foldr g b := by
   congr
 
-@[simp, grind] theorem foldl_push {f : β → α → β} {init : β} {xs : Vector α n} {a : α} :
+@[simp, grind =] theorem foldl_push {f : β → α → β} {init : β} {xs : Vector α n} {a : α} :
     (xs.push a).foldl f init = f (xs.foldl f init) a := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem foldr_push {f : α → β → β} {init : β} {xs : Vector α n} {a : α} :
+@[simp, grind =] theorem foldr_push {f : α → β → β} {init : β} {xs : Vector α n} {a : α} :
     (xs.push a).foldr f init = xs.foldr f (f a init) := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2490,21 +2490,21 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} :
     (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := foldrM_append
 
-@[simp, grind] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
+@[simp, grind =] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by
   cases xss using vector₂_induction
   simp [Array.foldl_flatten', Array.foldl_map']
 
-@[simp, grind] theorem foldr_flatten {f : α → β → β} {b} {xss : Vector (Vector α m) n} :
+@[simp, grind =] theorem foldr_flatten {f : α → β → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldr f b = xss.foldr (fun xs b => xs.foldr f b) b := by
   cases xss using vector₂_induction
   simp [Array.foldr_flatten', Array.foldr_map']
 
-@[simp, grind] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} :
+@[simp, grind =] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} :
     xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
   foldlM_reverse
 
-@[simp, grind] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} :
+@[simp, grind =] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
@@ -2629,7 +2629,7 @@ theorem back_append_left {xs : Vector α n} {ys : Vector α 0} [NeZero n] :
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_left _ h]
 
-@[simp, grind] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+@[simp, grind =] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp
@@ -2686,19 +2686,19 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_toList [BEq α] {xs : Vector α n} {x : α} :
     xs.toList.contains x = xs.contains x := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_toArray [BEq α] {xs : Vector α n} {x : α} :
     xs.toArray.contains x = xs.contains x := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_map [BEq β] {xs : Vector α n} {x : β} {f : α → β} :
     (xs.map f).contains x = xs.any (fun a => x == f a) := by
   rcases xs with ⟨xs⟩
@@ -2723,19 +2723,19 @@ theorem contains_append [BEq α] {xs : Vector α n} {ys : Vector α m} {x : α}
   rcases ys with ⟨ys, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatten [BEq α] {xs : Vector (Vector α n) m} {x : α} :
     (xs.flatten).contains x = xs.any fun xs => xs.contains x := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_reverse [BEq α] {xs : Vector α n} {x : α} :
     (xs.reverse).contains x = xs.contains x := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatMap [BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β} :
     (xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
   rcases xs with ⟨xs, rfl⟩
@@ -2747,7 +2747,7 @@ theorem contains_flatMap [BEq β] {xs : Vector α n} {f : α → Vector β m} {x
 
 @[simp] theorem pop_push {xs : Vector α n} {x : α} : (xs.push x).pop = xs := by simp [pop]
 
-@[simp, grind] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) :
+@[simp, grind =] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) :
     xs.pop[i] = xs[i] := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2908,15 +2908,15 @@ theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool
   unfold all
   apply allM_congr w h
 
-@[simp, grind] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
+@[simp, grind =] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
   cases xss using vector₂_induction
   simp
 
-@[simp, grind] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
+@[simp, grind =] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
   cases xss using vector₂_induction
   simp
 
-@[simp, grind] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+@[simp, grind =] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
     (xs.flatMap f).any p = xs.any fun a => (f a).any p := by
   rcases xs with ⟨xs⟩
   simp only [flatMap_mk, any_mk, Array.size_flatMap, size_toArray, Array.any_flatMap']
@@ -2925,7 +2925,7 @@ theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool
   congr
   simp [Vector.size_toArray]
 
-@[simp, grind] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+@[simp, grind =] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
     (xs.flatMap f).all p = xs.all fun a => (f a).all p := by
   rcases xs with ⟨xs⟩
   simp only [flatMap_mk, all_mk, Array.size_flatMap, size_toArray, Array.all_flatMap']
@@ -2934,11 +2934,11 @@ theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool
   congr
   simp [Vector.size_toArray]
 
-@[simp, grind] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
+@[simp, grind =] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
+@[simp, grind =] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -2974,7 +2974,7 @@ variable [BEq α]
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by simp
+@[simp, grind =] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by simp
 
 @[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
   simp
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 0b3b990388..5071fb6fb7 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -166,25 +166,25 @@ export LawfulGetElem (getElem?_def getElem!_def)
 instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
     LawfulGetElem coll idx elem valid where
 
-@[simp, grind] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind =] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
   have : Decidable (dom c i) := .isTrue h
   rw [getElem?_def]
   exact dif_pos h
 
-@[simp, grind] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind =] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
   have : Decidable (dom c i) := .isFalse h
   rw [getElem?_def]
   exact dif_neg h
 
-@[simp, grind] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind =] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
     c[i]! = c[i]'h := by
   have : Decidable (dom c i) := .isTrue h
   simp [getElem!_def, h]
 
-@[simp, grind] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind =] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
   have : Decidable (dom c i) := .isFalse h
   simp [getElem!_def, h]
@@ -291,11 +291,11 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) :
     getElem (a :: as) 0 h = a := rfl
 
-@[simp, grind]
+@[simp, grind =]
 theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) :=
     rfl
 
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
index 84ff1baf1f..d2e0838712 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -418,8 +418,16 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
         · exact Or.inr hf
     · simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
       split
-      next some_eq_none => grind
-      next l _ _ heq => grind [cases Bool]
+      next some_eq_none => simp at some_eq_none
+      next l _ _ heq =>
+        simp only [Option.some.injEq] at heq
+        rw [heq] at hl
+        specialize hl l.1
+        simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
+        by_cases hl2 : l.2
+        · simp only [← hl2, not_true, and_false] at hl
+        · simp only [Bool.not_eq_true] at hl2
+          simp only [← hl2, not_true, false_and] at hl
       · have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
           simp only [deleteOne]
           grind
@@ -438,7 +446,23 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
               grind
             apply Exists.intro ⟨idx, idx_in_bounds⟩
-            grind [unit]
+            by_cases id = idx
+            · next id_eq_idx =>
+              exfalso
+              have idx_in_bounds2 : idx < f.clauses.size := by
+                conv => rhs; rw [List.size_toArray]
+                exact hbound
+              simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
+                Array.getElem_toList] at heq
+              rw [hidx] at heq
+              simp only [Option.some.injEq] at heq
+              rw [← heq] at hl
+              specialize hl i
+              simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
+                Bool.not_eq_false, Bool.not_eq_true] at hl
+              by_cases b_val : b <;> simp [b_val] at hl
+            · next id_ne_idx =>
+              simp [id_ne_idx]; grind only [= Array.getElem_toList]
           · exact hf
         · exact Or.inr hf
 
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
index 32f8cce7b6..0d06bd83dc 100644
--- a/tests/lean/run/grind_option.lean
+++ b/tests/lean/run/grind_option.lean
@@ -18,8 +18,8 @@ example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by
 
 /--
 info: Try this:
-  grind only [Option.max_none_right,
-    Option.min_some_some, = Nat.min_def]
+  grind only [= Option.min_some_some,
+    = Option.max_none_right, = Nat.min_def]
 -/
 #guard_msgs in
 example : max (some 7) none = min (some 13) (some 7) := by grind?