diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 19198457c2..55c9c8a774 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -377,9 +377,9 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
     for g in newGoals do
       if mctx.isAnonymousMVar g then
         if numAnonymous == 1 then
-          mctx := mctx.renameMVar g parentTag
+          mctx := mctx.setMVarUserName g parentTag
         else
-          mctx := mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx)
+          mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
         idx := idx + 1
     pure mctx
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index eaf13917b5..aaccf4a912 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -418,8 +418,8 @@ def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do
   else
     return (← getLevelMVarDepth mvarId) != (← getMCtx).depth
 
-def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
-  modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName
+def setMVarUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
+  modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
 
 def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool :=
   return (← getMCtx).isExprAssigned mvarId
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index acf72a3b11..f586eb97c6 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -15,7 +15,7 @@ def getMVarTag (mvarId : MVarId) : MetaM Name :=
   return (← getMVarDecl mvarId).userName
 
 def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
-  modify fun s => { s with mctx := s.mctx.renameMVar mvarId tag }
+  modify fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag }
 
 def appendTag (tag : Name) (suffix : Name) : Name :=
   tag.modifyBase (· ++ suffix.eraseMacroScopes)
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index e1ce7a3620..0318ab1c35 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -349,7 +349,7 @@ def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) :
   let decl := mctx.getDecl mvarId
   { mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } }
 
-def renameMVar (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext :=
+def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext :=
   let decl := mctx.getDecl mvarId
   { mctx with
     decls := mctx.decls.insert mvarId { decl with userName := userName }