diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index b5d11e986a..1ef9926127 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -209,7 +209,14 @@ def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   unless binfo.isExplicit do
     e := e.setAppPPExplicit
   let aType ← inferType a
-  throwError "Application type mismatch: In the application{indentExpr e}\nthe final argument{indentExpr a}\n{← mkHasTypeButIsExpectedMsg aType expectedType}"
+  -- Clarify that `a` is "last" only if it may be confused with some preceding argument; otherwise,
+  -- avoid this wording because it may be misleading if more arguments follow `a`, e.g., if `f a` is
+  -- a subexpression of `f a b`
+  let argDescStr := if f.getAppArgs.any (· == a) then
+    m!"last{indentExpr a}\nargument "
+  else
+    m!"argument{indentExpr a}\n"
+  throwError "Application type mismatch: In the application{indentExpr e}\nthe {argDescStr}{← mkHasTypeButIsExpectedMsg aType expectedType}"
 
 def checkApp (f a : Expr) : MetaM Unit := do
   let fType ← inferType f
diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out
index 0950fe28cb..68c3dff208 100644
--- a/tests/lean/243.lean.expected.out
+++ b/tests/lean/243.lean.expected.out
@@ -1,6 +1,6 @@
 243.lean:2:10-2:14: error: Application type mismatch: In the application
   ⟨Bool, true⟩
-the final argument
+the argument
   true
 has type
   _root_.Bool : Type
@@ -8,7 +8,7 @@ but is expected to have type
   Bool : Type
 243.lean:13:7-13:8: error: Application type mismatch: In the application
   ⟨A, a⟩
-the final argument
+the argument
   a
 has type
   Foo.A : Type
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 6edd141d8e..d8b534b351 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -1,6 +1,6 @@
 283.lean:1:24-1:25: error: Application type mismatch: In the application
   f f
-the final argument
+the argument
   f
 has type
   ?m : Sort ?u
diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out
index fc9efe1015..11368e25f3 100644
--- a/tests/lean/389.lean.expected.out
+++ b/tests/lean/389.lean.expected.out
@@ -1,6 +1,6 @@
 389.lean:7:14-7:17: error: Application type mismatch: In the application
   getFoo bar
-the final argument
+the argument
   bar
 has type
   Bar Nat : Type
diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out
index 0177652ad6..c40e75e03e 100644
--- a/tests/lean/423.lean.expected.out
+++ b/tests/lean/423.lean.expected.out
@@ -1,6 +1,6 @@
 423.lean:3:35-3:40: error: Application type mismatch: In the application
   HAdd.hAdd a
-the final argument
+the argument
   a
 has type
   T : Sort u
@@ -8,7 +8,7 @@ but is expected to have type
   Nat : Type
 423.lean:5:37-5:38: error: Application type mismatch: In the application
   Add T
-the final argument
+the argument
   T
 has type
   Sort u : Type u
@@ -16,7 +16,7 @@ but is expected to have type
   Type ?u : Type (?u + 1)
 423.lean:5:47-5:48: error: Application type mismatch: In the application
   OfNat T
-the final argument
+the argument
   T
 has type
   Sort u : Type u
@@ -24,7 +24,7 @@ but is expected to have type
   Type ?u : Type (?u + 1)
 423.lean:5:55-5:60: error: Application type mismatch: In the application
   HAdd.hAdd a
-the final argument
+the argument
   a
 has type
   T : Sort u
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 2960ed07de..42f0d7836f 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -1,6 +1,6 @@
 autoPPExplicit.lean:2:26-2:31: error: Application type mismatch: In the application
   @Eq.trans α a (b = c)
-the final argument
+the argument
   b = c
 has type
   Prop : Type
diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out
index e218a20849..78835753d3 100644
--- a/tests/lean/doErrorMsg.lean.expected.out
+++ b/tests/lean/doErrorMsg.lean.expected.out
@@ -30,7 +30,7 @@ but is expected to have type
   ExceptT String (StateT Nat Id) String : Type
 doErrorMsg.lean:28:13-28:18: error: Application type mismatch: In the application
   Prod.mk false
-the final argument
+the argument
   false
 has type
   Bool : Type
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
index c474f90fcf..73cc58de9f 100644
--- a/tests/lean/doIssue.lean.expected.out
+++ b/tests/lean/doIssue.lean.expected.out
@@ -12,7 +12,7 @@ but is expected to have type
   IO PUnit : Type
 doIssue.lean:18:7-18:20: error: Application type mismatch: In the application
   pure (xs.set! 0 1)
-the final argument
+the argument
   xs.set! 0 1
 has type
   Array Nat : Type
diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out
index 99a65bf8a3..c85affabed 100644
--- a/tests/lean/elseifDoErrorPos.lean.expected.out
+++ b/tests/lean/elseifDoErrorPos.lean.expected.out
@@ -1,6 +1,6 @@
 elseifDoErrorPos.lean:4:10-4:11: error: Application type mismatch: In the application
   @ite ?m x
-the final argument
+the argument
   x
 has type
   Nat : Type
@@ -8,7 +8,7 @@ but is expected to have type
   Prop : Type
 elseifDoErrorPos.lean:7:11-7:14: error: Application type mismatch: In the application
   pure "a"
-the final argument
+the argument
   "a"
 has type
   String : Type
diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out
index b03c41cf95..403b7e91d7 100644
--- a/tests/lean/evalSorry.lean.expected.out
+++ b/tests/lean/evalSorry.lean.expected.out
@@ -1,7 +1,7 @@
 1
 evalSorry.lean:5:33-5:34: error: Application type mismatch: In the application
   f x
-the final argument
+the argument
   x
 has type
   String : Type
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index dcf5aae0f0..64e2cd56c7 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -4,7 +4,7 @@ macroSwizzle.lean:4:7-4:23: error: failed to synthesize
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: Application type mismatch: In the application
   Nat.succ "x"
-the final argument
+the argument
   "x"
 has type
   String : Type
diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index 97528d1899..59dc8d648c 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/tests/lean/modBug.lean.expected.out
@@ -1,6 +1,6 @@
 modBug.lean:1:48-1:64: error: Application type mismatch: In the application
   Nat.zero_ne_one (Nat.mod_zero 1)
-the final argument
+the argument
   Nat.mod_zero 1
 has type
   1 % 0 = 1 : Prop
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out
index d0006c70d7..17346b81c8 100644
--- a/tests/lean/motiveNotTypeCorect.lean.expected.out
+++ b/tests/lean/motiveNotTypeCorect.lean.expected.out
@@ -2,7 +2,7 @@ motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not
   fun _a => P _a d
 Error: Application type mismatch: In the application
   P _a d
-the final argument
+the argument
   d
 has type
   D (f t) : Type
diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out
index 648ee99b11..d8e8eabc97 100644
--- a/tests/lean/nameArgErrorIssue.lean.expected.out
+++ b/tests/lean/nameArgErrorIssue.lean.expected.out
@@ -1,7 +1,7 @@
 bla 5 2 : Nat
 nameArgErrorIssue.lean:5:20-5:24: error: Application type mismatch: In the application
   bla "hi"
-the final argument
+the argument
   "hi"
 has type
   String : Type
@@ -10,7 +10,7 @@ but is expected to have type
 bla sorry 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: Application type mismatch: In the application
   bla "hi"
-the final argument
+the argument
   "hi"
 has type
   String : Type
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index f1d0392bc7..4e3f66b468 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -1,8 +1,8 @@
 namedHoles.lean:9:12-9:14: error: Application type mismatch: In the application
   f ?x ?x
-the final argument
+the last
   ?x
-has type
+argument has type
   Nat : Type
 but is expected to have type
   Bool : Type
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 7b8952b48a..c07a90156a 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -1,6 +1,6 @@
 phashmap_inst_coherence.lean:12:53-12:54: error: Application type mismatch: In the application
   m.find?
-the final argument
+the argument
   m
 has type
   @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type
diff --git a/tests/lean/run/439.lean b/tests/lean/run/439.lean
index 809aead580..fd3333876e 100644
--- a/tests/lean/run/439.lean
+++ b/tests/lean/run/439.lean
@@ -44,7 +44,7 @@ variable (fn' : Fn ((p : P) -> B.fn p -> B.fn p) ({p : P} -> B.fn p -> B.fn p))
 /--
 error: Application type mismatch: In the application
   fn'.imp p
-the final argument
+the argument
   p
 has type
   P : Sort u
diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index cbe984b4a9..6178bba1f8 100644
--- a/tests/lean/run/4405.lean
+++ b/tests/lean/run/4405.lean
@@ -5,7 +5,7 @@ set_option pp.mvars false
 /--
 error: Application type mismatch: In the application
   ⟨Nat.lt_irrefl (?_ n), Fin.is_lt ?_⟩
-the final argument
+the argument
   Fin.is_lt ?_
 has type
   ↑?_ < ?_ : Prop
diff --git a/tests/lean/run/4670.lean b/tests/lean/run/4670.lean
index 6a457307eb..e78e788e9f 100644
--- a/tests/lean/run/4670.lean
+++ b/tests/lean/run/4670.lean
@@ -13,7 +13,7 @@ Was printing `true.out`, but it should have been `Foo.out true`.
 /--
 error: Application type mismatch: In the application
   Foo.out true
-the final argument
+the argument
   true
 has type
   Bool : Type
@@ -31,7 +31,7 @@ def Foo.out' (f : Foo) : Nat := f.out
 /--
 error: Application type mismatch: In the application
   Foo.out' true
-the final argument
+the argument
   true
 has type
   Bool : Type
diff --git a/tests/lean/run/4888.lean b/tests/lean/run/4888.lean
index 08ea4f44c3..3a34394da7 100644
--- a/tests/lean/run/4888.lean
+++ b/tests/lean/run/4888.lean
@@ -7,7 +7,7 @@ https://github.com/leanprover/lean4/issues/4888
 /--
 error: Application type mismatch: In the application
   Nat.succ True
-the final argument
+the argument
   True
 has type
   Prop : Type
diff --git a/tests/lean/run/DVec.lean b/tests/lean/run/DVec.lean
index 703df1cd75..fcc1a1673d 100644
--- a/tests/lean/run/DVec.lean
+++ b/tests/lean/run/DVec.lean
@@ -42,7 +42,7 @@ example (v : Vec Nat 1) : Nat :=
 /--
 error: Application type mismatch: In the application
   @DVec.hd ?_ v
-the final argument
+the argument
   v
 has type
   Vec Nat 1 : Type
diff --git a/tests/lean/run/check.lean b/tests/lean/run/check.lean
index bee9b835f9..8c9b58643e 100644
--- a/tests/lean/run/check.lean
+++ b/tests/lean/run/check.lean
@@ -35,7 +35,7 @@ elab "elab_1eq1" : term => return expr_1eq1
 /--
 error: Application type mismatch: In the application
   @Eq Nat
-the final argument
+the argument
   Nat
 has type
   Type : Type 1
@@ -47,7 +47,7 @@ but is expected to have type
 /--
 error: Application type mismatch: In the application
   @Eq Nat
-the final argument
+the argument
   Nat
 has type
   Type : Type 1
diff --git a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean b/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean
index d1480e7447..af0b39f639 100644
--- a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean
+++ b/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean
@@ -2,9 +2,9 @@ def foo (x : Nat) (y : Bool) (z : Nat) (w : Nat) := ()
 /--
 error: Application type mismatch: In the application
   foo 1 true true
-the final argument
+the last
   true
-has type
+argument has type
   Bool : Type
 but is expected to have type
   Nat : Type
diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean
index 4579cce674..de42de10f7 100644
--- a/tests/lean/run/issue8213.lean
+++ b/tests/lean/run/issue8213.lean
@@ -19,7 +19,7 @@ error: Failed to realize constant myTest.fun_cases:
     ⏎
       Application type mismatch: In the application
         motive mmotive x✝ h_1
-      the final argument
+      the argument
         h_1
       has type
         (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean
index 79097242cf..72764c3200 100644
--- a/tests/lean/run/scopedunifhint.lean
+++ b/tests/lean/run/scopedunifhint.lean
@@ -30,7 +30,7 @@ def x : Nat := 10
 /--
 error: Application type mismatch: In the application
   mul ?_ x
-the final argument
+the argument
   x
 has type
   Nat : Type
@@ -43,7 +43,7 @@ but is expected to have type
 /--
 error: Application type mismatch: In the application
   mul ?_ (x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type
@@ -58,7 +58,7 @@ local infix:65 (priority := high) "*" => mul
 /--
 error: Application type mismatch: In the application
   ?_*x
-the final argument
+the argument
   x
 has type
   Nat : Type
@@ -76,7 +76,7 @@ open Algebra -- activate unification hints
 /--
 error: Application type mismatch: In the application
   ?_*(x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type
@@ -104,7 +104,7 @@ end Sec1
 /--
 error: Application type mismatch: In the application
   ?_*(x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index dcfb521bab..233b10301f 100644
--- a/tests/lean/run/variable.lean
+++ b/tests/lean/run/variable.lean
@@ -138,7 +138,7 @@ set_option pp.mvars false in
 /--
 error: Application type mismatch: In the application
   ToString True
-the final argument
+the argument
   True
 has type
   Prop : Type
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index 3dc3165fbc..883faffb77 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/tests/lean/simpArgTypeMismatch.lean.expected.out
@@ -1,6 +1,6 @@
 simpArgTypeMismatch.lean:3:29-3:33: error: Application type mismatch: In the application
   decide_eq_false Unit
-the final argument
+the argument
   Unit
 has type
   Type : Type 1
diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out
index 3963e4240e..30fcbce94f 100644
--- a/tests/lean/sorryAtError.lean.expected.out
+++ b/tests/lean/sorryAtError.lean.expected.out
@@ -1,6 +1,6 @@
 sorryAtError.lean:13:46-13:47: error: Application type mismatch: In the application
   ty.ty Γ
-the final argument
+the argument
   Γ
 has type
   x.ty.ctx : Type