diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 875ef9c05e..7de8b1b825 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -63,7 +63,7 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 /-! ### size -/
 
-@[grind →] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
+theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
 
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 812d5d69d8..11e61a8385 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -486,7 +486,7 @@ abbrev toArray_mkVector := @toArray_replicate
 `Vector.ext` is an extensionality theorem.
 Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
 -/
-@[ext]
+@[ext, grind ext]
 protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → xs[i] = ys[i]) : xs = ys := by
   apply Vector.toArray_inj.1
   apply Array.ext
diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean
index ecf5a71ea7..1a862876d9 100644
--- a/src/Init/Ext.lean
+++ b/src/Init/Ext.lean
@@ -82,6 +82,8 @@ end Lean
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq Array.ext
 
+attribute [grind ext] Array.ext
+
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
 
diff --git a/tests/lean/grind/grind_palindrome.lean b/tests/lean/grind/grind_palindrome.lean
new file mode 100644
index 0000000000..749284c037
--- /dev/null
+++ b/tests/lean/grind/grind_palindrome.lean
@@ -0,0 +1,37 @@
+set_option grind.warning false
+
+def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
+
+def checkPalin1 (xs : Array Nat) : Bool :=
+  go 0
+where
+  go  (i : Nat) :=
+    if h : i < xs.size / 2 then
+      if xs[i] = xs[xs.size - 1 - i] then
+        go (i + 1)
+      else
+        false
+    else
+      true
+
+-- This give the more natural proof that we'd like to give in `tests/run/grind_palindrome2.lean`,
+-- but in which `grind` currently fails.
+
+theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
+  unfold checkPalin1
+  suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size - i) → xs[j] = xs[xs.size - 1 - j] by
+    grind [IsPalindrome]
+  intro i
+  fun_induction checkPalin1.go
+  · grind (splits := 14)
+    -- fails, but it would be nice to succeed! The key observations are:
+    -- [eqc] True propositions ▼
+    --   [prop] ∀ (a : Nat) (b : a + 1 ≤ xs.toList.length - x), a + 1 ≤ x ∨ xs[a] = xs[xs.toList.length - (a + 1)]
+    -- [eqc] False propositions ▼
+    --   [prop] xs[x] = xs[xs.toList.length - (x + 1)]
+    -- Instantiating the `∀` with `a := x`, we can then easily prove `a + 1 ≤ xs.toList.length - x` and
+    -- prove that it's not the case that `a + 1 ≤ x`, so we get `xs[x] = xs[xs.toList.length - (x + 1)]`,
+    -- which is false.
+  · grind
+    -- The same argument should apply here.
+  · grind
diff --git a/tests/lean/run/grind_palindrome2.lean b/tests/lean/run/grind_palindrome2.lean
index de555a2854..87649c2b81 100644
--- a/tests/lean/run/grind_palindrome2.lean
+++ b/tests/lean/run/grind_palindrome2.lean
@@ -14,15 +14,12 @@ where
     else
       true
 
-example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
-    xs[j] = xs[xs.size - 1 - j] := by
-  grind
-
-attribute [grind ext] Array.ext -- TODO: should we mark it by default?
-
-theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
+-- This works nicely, but there is some human assistance here:
+-- on the right hand side of the `suffices` we've asserted it's enough to check up to `j < xs.size / 2`
+-- while the "natural" statement would be all the way to `j < xs.size - i`.
+theorem checkPalin1_correct : checkPalin1 xs = true ↔ IsPalindrome xs := by
   unfold checkPalin1
   suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size / 2) → xs[j] = xs[xs.size - 1 - j] by
     grind [IsPalindrome]
   intro i
-  fun_induction checkPalin1.go <;> grind
+  fun_induction checkPalin1.go with grind