fix: simplify isCasesAttrCandidate? in grind (#8415)

The behavior was counterintuitive.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -70,20 +70,9 @@ def getCasesTypes : CoreM CasesTypes :=
 def isSplit (declName : Name) : CoreM Bool := do
   return (← getCasesTypes).isSplit declName
 
-private def getAlias? (value : Expr) : MetaM (Option Name) :=
-  lambdaTelescope value fun _ body => do
-    if let .const declName _ := body.getAppFn' then
-      return some declName
-    else
-      return none
-
 partial def isCasesAttrCandidate? (declName : Name) (eager : Bool) : CoreM (Option Name) := do
   match (← getConstInfo declName) with
   | .inductInfo info => if !info.isRec || !eager then return some declName else return none
-  | .defnInfo info =>
-    let some declName ← getAlias? info.value |>.run' {} {}
-      | return none
-    isCasesAttrCandidate? declName eager
   | _ => return none
 
 def isCasesAttrCandidate (declName : Name) (eager : Bool) : CoreM Bool := do

tests/lean/run/grind_palindrome2.lean

@@ -18,11 +18,11 @@ example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j
     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
   unfold checkPalin1
   suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size / 2) → xs[j] = xs[xs.size - 1 - j] by
-    -- We need array extensionality. TODO: easy way to enable array extensionality, `extAll` enables all [ext] theorems
-    -- TODO: `IsPalindrome` (without `.eq_1`) produces bad error message.
-    grind +extAll [IsPalindrome.eq_1]
+    grind [IsPalindrome]
   intro i
   fun_induction checkPalin1.go <;> grind