fix: case splitting on data

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

diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean
index 6124bbe..8b4d472 100644
--- a/src/Lean/Meta/Tactic/Grind/Cases.lean
+++ b/src/Lean/Meta/Tactic/Grind/Cases.lean
@@ -85,6 +85,20 @@
   let s ← s.eraseDecl declName
   modifyEnv fun env => casesExt.modifyState env fun _ => s
 
+/--
+We say a free variable is "simple" to be processed by the cases tactic IF:
+- It is the latest and consequently there are no forward dependencies, OR
+- It is not a proposion.
+-/
+private def isSimpleFVar (e : Expr) : MetaM Bool := do
+  let .fvar fvarId := e | return false
+  let decl ← fvarId.getDecl
+  if decl.index == (← getLCtx).numIndices - 1 then
+    -- It is the latest free variable, so there are no forward dependencies
+    return true
+  else
+    -- It is pointless to add an auxiliary equality if `e`s type is a proposition
+    isProp decl.type
 
 /--
 The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
@@ -132,12 +146,17 @@
     let s ← generalizeIndices' mvarId e
     s.mvarId.withContext do
       k s.mvarId s.fvarId s.indicesFVarIds
-  else if let .fvar fvarId := e then
-    k mvarId fvarId #[]
+  else if (← isSimpleFVar e) then
+    -- We don't need to revert anything.
+    k mvarId e.fvarId! #[]
   else
-    let mvarId ← mvarId.assert (← mkFreshUserName `x) type e
+    let mvarId ← if (← isProof e) then
+      mvarId.assert (← mkFreshUserName `x) type e
+    else
+      mvarId.assertExt (← mkFreshUserName `x) type e
     let (fvarId, mvarId) ← mvarId.intro1
     mvarId.withContext do k mvarId fvarId #[]
+
 where
   throwInductiveExpected {α} (type : Expr) : MetaM α := do
     throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {e}{indentExpr type}"

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

diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index dce9503..564284b 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -97,16 +97,19 @@
       return .resolved
     if let some info := isMatcherAppCore? (← getEnv) e then
       return .ready info.numAlts
-    let .const declName .. := e.getAppFn | unreachable!
-    if let some info ← isInductivePredicate? declName then
-      if (← isEqTrue e) then
-        return .ready info.ctors.length info.isRec
+    if let .const declName .. := e.getAppFn then
+      if let some info ← isInductivePredicate? declName then
+        if (← isEqTrue e) then
+          return .ready info.ctors.length info.isRec
     if e.isFVar then
       let type ← whnfD (← inferType e)
+      trace[Meta.debug] "1. {e}"
       let report : GoalM Unit := do
         reportIssue "cannot perform case-split on {e}, unexpected type{indentExpr type}"
       let .const declName _ := type.getAppFn | report; return .resolved
+      trace[Meta.debug] "2. {e}"
       let .inductInfo info ← getConstInfo declName | report; return .resolved
+      trace[Meta.debug] "3. {e}"
       return .ready info.ctors.length info.isRec
     return .notReady
 
@@ -162,7 +165,11 @@
       return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
     else
       return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
-  | _ => return mkOfEqTrueCore c (← mkEqTrueProof c)
+  | _ =>
+    if (← isEqTrue c) then
+      return mkOfEqTrueCore c (← mkEqTrueProof c)
+    else
+      return c
 
 /-- Introduces new hypotheses in each goal. -/
 private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do

tests/lean/run/grind_split_data.lean

diff --git a/tests/lean/run/grind_split_data.lean b/tests/lean/run/grind_split_data.lean
new file mode 100644
index 0000000..168e093
--- /dev/null
+++ b/tests/lean/run/grind_split_data.lean
@@ -0,0 +1,13 @@
+inductive C where
+  | a | b | c
+
+def f : C → Nat
+  | .a => 2
+  | .b => 3
+  | .c => 4
+
+example : f .a > 1 := by
+  grind [f]
+
+example : f x > 1 := by
+  grind [f, C]