diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 1b38f36123..7cd51782f7 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -97,7 +97,7 @@ syntax (name := arg) "arg " argArg : conv
 
 /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
 to target `e`, introducing name `x` in the process. -/
-syntax (name := ext) "ext" (ppSpace colGt ident)* : conv
+syntax (name := ext) "ext" (ppSpace colGt binderIdent)* : conv
 
 /-- `change t'` replaces the target `t` with `t'`,
 assuming `t` and `t'` are definitionally equal. -/
@@ -281,9 +281,9 @@ macro "left" : conv => `(conv| lhs)
 /-- `right` traverses into the right argument. Synonym for `rhs`. -/
 macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
-macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*)
+macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
 
-syntax enterArg := ident <|> argArg
+syntax enterArg := binderIdent <|> argArg
 
 /-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
 It is a shorthand for other conv tactics as follows:
diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 08eb606d99..d55a242a0e 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -318,7 +318,11 @@ private def ext (userName? : Option Name) : TacticM Unit := do
     ext none
   else
     for id in ids do
-      withRef id <| ext id.getId
+      let userName? :=
+        match id with
+        | `(binderIdent| $id:ident) => some id.getId
+        | _ => none
+      withRef id <| ext userName?
 
 -- syntax (name := enter) "enter" " [" enterArg,+ "]" : conv
 @[builtin_tactic Lean.Parser.Tactic.Conv.enter] def evalEnter : Tactic := fun stx => do
@@ -334,8 +338,8 @@ private def ext (userName? : Option Name) : TacticM Unit := do
     -- show state up to (incl.) next `,` and show errors on `enterArg`
     withTacticInfoContext (mkNullNode #[enterArg, sep]) <| withRef enterArg do
       match enterArg with
-      | `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic (← `(conv| arg $arg))
-      | `(Parser.Tactic.Conv.enterArg| $id:ident)   => evalTactic (← `(conv| ext $id))
+      | `(Parser.Tactic.Conv.enterArg| $arg:argArg)     => evalTactic (← `(conv| arg $arg))
+      | `(Parser.Tactic.Conv.enterArg| $id:binderIdent) => evalTactic (← `(conv| ext $id))
       | _ => pure ()
 
 end Lean.Elab.Tactic.Conv