diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 050581e1b6..648ed62c64 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -169,9 +169,11 @@ structure State where
     -- fun x => f x 5
     ```
     `etaArgs` stores the fresh free variables for implementing the eta-expansion.
+    Each pair records the name to use for the binding and the fvar for the argument.
+
     When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`.
   -/
-  etaArgs              : Array Expr   := #[]
+  etaArgs              : Array (Name × Expr)   := #[]
   /-- Metavariables that we need to set the error context using the application being built. -/
   toSetErrorCtx        : Array MVarId := #[]
   /-- Metavariables for the instance implicit arguments that have already been processed. -/
@@ -420,7 +422,8 @@ private def finalize : M Expr := do
   for mvarId in s.toSetErrorCtx do
     registerMVarErrorImplicitArgInfo mvarId ref e
   if !s.etaArgs.isEmpty then
-    e ← mkLambdaFVars s.etaArgs e
+    e ← mkLambdaFVars (s.etaArgs.map (·.2)) e
+    e := e.updateBinderNames (s.etaArgs.map (some <| ·.1)).toList
   /-
     Remark: we should not use `s.fType` as `eType` even when
     `s.etaArgs.isEmpty`. Reason: it may have been unfolded.
@@ -562,8 +565,9 @@ mutual
   private partial def addEtaArg (argName : Name) : M Expr := do
     let n    ← getBindingName
     let type ← getArgExpectedType
-    withLocalDeclD n type fun x => do
-      modify fun s => { s with etaArgs := s.etaArgs.push x }
+    -- Use a fresh name to ensure that the remaining arguments can't capture this parameter's name.
+    withLocalDeclD (← Core.mkFreshUserName n) type fun x => do
+      modify fun s => { s with etaArgs := s.etaArgs.push (n, x) }
       addNewArg argName x
       main
 
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index c5aa567070..201b09b3da 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -306,7 +306,7 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
 
 @[builtin_tactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx =>
   match stx with
-  | `(tactic| apply $e) => evalApplyLikeTactic (·.apply (term? := some m!"`{e}`")) e
+  | `(tactic| apply $t) => evalApplyLikeTactic (fun g e => g.apply e (term? := some m!"`{e}`")) t
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun _ =>
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 838b8f1524..c2b34bd068 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1346,7 +1346,7 @@ def inferImplicit (e : Expr) (numParams : Nat) (considerRange : Bool) : Expr :=
   | e, _ => e
 
 /--
-Uses `newBinderInfos` to update the binder infos of the first `numParams` foralls.
+Uses `binderInfos?` to update the binder infos of the corresponding forall expressions.
 -/
 def updateForallBinderInfos (e : Expr) (binderInfos? : List (Option BinderInfo)) : Expr :=
   match e, binderInfos? with
@@ -1356,6 +1356,21 @@ def updateForallBinderInfos (e : Expr) (binderInfos? : List (Option BinderInfo))
     Expr.forallE n d b bi
   | e, _ => e
 
+/--
+Uses `binderNames?` to update the binder names of the corresponding lambda and forall expressions.
+-/
+def updateBinderNames (e : Expr) (binderNames? : List (Option Name)) : Expr :=
+  match e, binderNames? with
+  | Expr.forallE n d b bi, newN? :: binderNames? =>
+    let b := updateBinderNames b binderNames?
+    let n := newN?.getD n
+    Expr.forallE n d b bi
+  | Expr.lam n d b bi, newN? :: binderNames? =>
+    let b := updateBinderNames b binderNames?
+    let n := newN?.getD n
+    Expr.lam n d b bi
+  | e, _ => e
+
 /--
 Instantiates the loose bound variables in `e` using the `subst` array,
 where a loose `Expr.bvar i` at "binding depth" `d` is instantiated with `subst[i - d]` if `0 <= i - d < subst.size`,
diff --git a/tests/lean/run/5475.lean b/tests/lean/run/5475.lean
index a194038a7e..47ea0cf417 100644
--- a/tests/lean/run/5475.lean
+++ b/tests/lean/run/5475.lean
@@ -12,7 +12,7 @@ Formerly, argument `x` appeared as `_fvar.123`
 def f {α β : Type} (x: α) (y: β) : α := x
 /--
 error: don't know how to synthesize implicit argument `α`
-  @f ?_ Nat x Nat.zero
+  @f ?_ Nat x✝ Nat.zero
 context:
 ⊢ Type
 ---
diff --git a/tests/lean/run/6373.lean b/tests/lean/run/6373.lean
new file mode 100644
index 0000000000..b8230d8f0e
--- /dev/null
+++ b/tests/lean/run/6373.lean
@@ -0,0 +1,50 @@
+/-!
+# Test for issue 6373, variable capture for app elaborator eta feature
+
+https://github.com/leanprover/lean4/issues/6373
+-/
+
+def sum3 (x y z : Nat) : Nat := x + y + z
+
+/-!
+The following two used to elaborate differently.
+Now in the second, we can see that the `x` in the `fun` (from the eta feature), does not shadow the `x` in the `let`.
+Note that in both, `y` can still be used as a named argument.
+-/
+/--
+info: fun x =>
+  (let w := 15;
+    fun x y => sum3 x y w)
+    x 3 : Nat → Nat
+-/
+#guard_msgs in
+#check (let w := 15; sum3 (z := w)) (y := 3)
+/--
+info: fun x =>
+  (let x := 15;
+    fun x_1 y => sum3 x_1 y x)
+    x 3 : Nat → Nat
+-/
+#guard_msgs in
+#check (let x := 15; sum3 (z := x)) (y := 3)
+
+/-!
+Verifying that each evaluates to the same value when evaluated at `0`.
+The second used to evaluate to `3` instead of `18`.
+-/
+/-- info: 18 -/
+#guard_msgs in
+#eval (let w := 15; sum3 (z := w)) (y := 3) <| 0
+/-- info: 18 -/
+#guard_msgs in
+#eval (let x := 15; sum3 (z := x)) (y := 3) <| 0
+
+/-!
+Same verification, but make sure that `0` can be passed as a named argument.
+-/
+/-- info: 18 -/
+#guard_msgs in
+#eval (let w := 15; sum3 (z := w)) (y := 3) (x := 0)
+/-- info: 18 -/
+#guard_msgs in
+#eval (let x := 15; sum3 (z := x)) (y := 3) (x := 0)
diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean
index faf7c41daa..1948df974a 100644
--- a/tests/lean/run/funind_proof.lean
+++ b/tests/lean/run/funind_proof.lean
@@ -41,7 +41,7 @@ info: Term.replaceConst.induct (a : String) (motive1 : Term → Prop) (motive2 :
 #check replaceConst.induct
 
 theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  apply replaceConst.induct
+  apply replaceConst.induct (a := a)
     (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es)
   case case1 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *]
@@ -58,7 +58,7 @@ theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceCon
     simp [replaceConstLst, numConstsLst, *]
 
 theorem numConsts_replaceConst' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  apply replaceConst.induct
+  apply replaceConst.induct (a := a)
     (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es)
   <;> intros <;> simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]