From ff59a68774052f5e442538ef6ced8751d0b6d0f3 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 5 Nov 2024 12:26:43 -0800
Subject: [PATCH 1/2] fix: `arg` conv tactic misreported number of arguments on
 error

---
 src/Lean/Elab/Tactic/Conv/Congr.lean |  2 +-
 tests/lean/run/conv_arg.lean         | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index ab68579c7f34..407b62a65f0b 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -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:])
 
diff --git a/tests/lean/run/conv_arg.lean b/tests/lean/run/conv_arg.lean
index bd1642346eb5..c9237f09bee0 100644
--- a/tests/lean/run/conv_arg.lean
+++ b/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 arguments 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.

From 3edd7013e0cefcee2ce97b5a15893cbae5ea68ed Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 5 Nov 2024 12:31:27 -0800
Subject: [PATCH 2/2] fix plural

---
 src/Lean/Elab/Tactic/Conv/Congr.lean | 2 +-
 tests/lean/run/conv_arg.lean         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 407b62a65f0b..08eb606d991e 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/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
diff --git a/tests/lean/run/conv_arg.lean b/tests/lean/run/conv_arg.lean
index c9237f09bee0..6e6cf576bbbc 100644
--- a/tests/lean/run/conv_arg.lean
+++ b/tests/lean/run/conv_arg.lean
@@ -73,7 +73,7 @@ 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 arguments but the index is out of bounds -/
+/-- 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 =>