chore: improve grind case-split trace

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

@@ -146,8 +146,8 @@ private def ppCasesTrace : M Unit := do
   let goal ← read
   unless goal.casesTrace.isEmpty do
     let mut msgs := #[]
-    for (e, num) in goal.casesTrace.reverse do
-      msgs := msgs.push <| .trace { cls := `cases } m!"[{num}]: {e}" #[]
+    for { expr, i , num } in goal.casesTrace.reverse do
+      msgs := msgs.push <| .trace { cls := `cases } m!"[{i+1}/{num}]: {expr}" #[]
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do

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

@@ -196,7 +196,7 @@ def splitNext : GrindTactic := fun goal => do
       cases (← get).mvarId major
     let goal ← get
     let numSubgoals := mvarIds.length
-    let goals := mvarIds.map fun mvarId => { goal with mvarId, casesTrace := (c, numSubgoals) :: goal.casesTrace }
+    let goals := mvarIds.mapIdx fun i mvarId => { goal with mvarId, casesTrace := { expr := c, i, num := numSubgoals } :: goal.casesTrace }
     let goals ← introNewHyp goals [] genNew
     return some goals
   return goals?

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

@@ -434,6 +434,13 @@ structure Canon.State where
   proofCanon : PHashMap Expr Expr := {}
   deriving Inhabited
 
+/-- Trace information for a case split. -/
+structure CaseTrace where
+  expr : Expr
+  i    : Nat
+  num  : Nat
+  deriving Inhabited
+
 structure Goal where
   mvarId       : MVarId
   canon        : Canon.State := {}
@@ -494,7 +501,7 @@ structure Goal where
   Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
   applications that generated only 1 subgoal.
   -/
-  casesTrace : List (Expr × Nat) := []
+  casesTrace : List CaseTrace := []
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

tests/lean/grind_guide.lean.expected.out

@@ -73,7 +73,7 @@ h : x = 0
         1}
     [eqc] {x, 0}
   [cases] Case analyses
-    [cases] [2]: match x with
+    [cases] [1/2]: match x with
         | 0 => 1
         | n.succ => 2
   [ematch] E-matching patterns

tests/lean/run/grind_pre.lean

@@ -180,8 +180,8 @@ h : ¬r
     [prop] q
     [prop] r
   [cases] Case analyses
-    [cases] [1]: p = r
-    [cases] [2]: ¬r ∨ p
+    [cases] [1/1]: p = r
+    [cases] [1/2]: ¬r ∨ p
 [grind] Issues
   [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/

tests/lean/run/grind_split_issue.lean

@@ -23,7 +23,7 @@ h : HEq ⋯ ⋯
   [eqc] Equivalence classes
     [eqc] {s, 0}
   [cases] Case analyses
-    [cases] [2]: X c 0
+    [cases] [1/2]: X c 0
 [grind] Issues
   [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/