This PR fixes a regression introduced in #7166 where, after fixed and
varying
parameters were allowed to be reordered, three places in
`Lean.Elab.Structural.FindRecArg` still indexed the concatenation `xs ++
ys`
with `recArgInfo.recArgPos` even though `recArgPos` refers to the
original
parameter order. With fixed parameters interleaved with the structural
argument, this picked the wrong element: error messages named the wrong
parameter, and `argsInGroup`'s nested-inductive recognition silently
rejected
otherwise-valid mutual definitions.
All three sites now use `recArgInfo.fixedParamPerm.buildArgs xs ys` so
the
index matches `recArgPos` and `indicesPos`.
Closes#13729.
