fix: arg conv tactic misreported number of arguments on error (#5968)

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -200,7 +200,7 @@ where
     if explicit then
       let i := if i > 0 then i - 1 else i + xs.size
       if i < 0 || i ≥ xs.size then
-        throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {xs.size} argument(s) but the index is out of bounds"
       let idx := i.natAbs
       return (mkAppN f xs[0:idx], xs[idx:])
     else
@@ -217,7 +217,7 @@ where
           explicitIdxs := explicitIdxs.push k
       let i := if i > 0 then i - 1 else i + explicitIdxs.size
       if i < 0 || i ≥ explicitIdxs.size then
-        throwError "invalid '{tacticName}' tactic, application has {xs.size} explicit argument(s) but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {explicitIdxs.size} explicit argument(s) but the index is out of bounds"
       let idx := explicitIdxs[i.natAbs]!
       return (mkAppN f xs[0:idx], xs[idx:])
 

tests/lean/run/conv_arg.lean

@@ -61,6 +61,24 @@ example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by
     enter [1, @2]
     rw [h]
 
+/-!
+Out of bounds errors.
+-/
+
+/--
+error: invalid 'arg' tactic, application has 1 explicit argument(s) but the index is out of bounds
+-/
+#guard_msgs in
+example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by
+  conv =>
+    enter [1, 6]
+
+/-- error: invalid 'arg' tactic, application has 2 argument(s) but the index is out of bounds -/
+#guard_msgs in
+example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by
+  conv =>
+    enter [1, @6]
+
 /-!
 Issue https://github.com/leanprover/lean4/issues/5871
 The `arg` tactic was `congr` theorems, which was too restrictive.