fix: handle multi-discriminant casesOn in WF unfold equation generation

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -73,8 +73,9 @@ def splitMatchOrCasesOn (mvarId : MVarId) (e : Expr) (matcherInfo : MatcherInfo)
   if (← isMatcherApp e) then
     Split.splitMatch mvarId e
   else
-    assert! matcherInfo.numDiscrs = 1
-    let discr := e.getAppArgs[matcherInfo.numParams + 1]!
+    -- For casesOn, the last discriminant is the major premise;
+    -- `cases` will handle any index discriminants automatically.
+    let discr := e.getAppArgs[matcherInfo.numParams + matcherInfo.numDiscrs]!
     assert! discr.isFVar
     let subgoals ← mvarId.cases discr.fvarId!
     return subgoals.map (·.mvarId) |>.toList

tests/elab/issue13015.lean

@@ -0,0 +1,24 @@
+-- Mutually recursive definitions using casesOn on indexed types should not panic.
+-- https://github.com/leanprover/lean4/issues/13015
+
+inductive Vect (α : Type u) : Nat → Type u
+  | nil  : Vect α 0
+  | cons : α → {n : Nat} → Vect α n → Vect α (n+1)
+
+mutual
+def zipWithAux (f : α → β → γ) (a : α) (as : Vect α m) (bs : Vect β n) : n = m + 1 → γ × Vect γ m :=
+  Vect.casesOn (motive := λ k _ ↦ k = m + 1 → γ × Vect γ m) bs
+    (nil := λ h ↦ Nat.noConfusion h)
+    (cons := λ (b : β) (k : Nat) (bs : Vect β k) h ↦
+      Nat.noConfusion h (λ h1 : k = m ↦
+        ((f a b), (zipWith f as (h1 ▸ bs) rfl)))
+    )
+
+def zipWith (f : α → β → γ) {n : Nat} (as : Vect α n) (bs : Vect β n) : n = n → Vect γ n :=
+  Vect.casesOn (motive := λ m _ ↦ n = m → Vect γ m) as
+    (nil := λ _ ↦ Vect.nil)
+    (cons := λ (a : α) (m : Nat) (as : Vect α m) h ↦
+      let p := zipWithAux f a as bs h
+      Vect.cons p.1 p.2
+    )
+end