fix: appendTagSuffix operation

src/Lean/Meta/Tactic/Apply.lean

@@ -43,7 +43,7 @@ unless parentTag.isAnonymous $
     unlessM (isExprMVarAssigned newMVarId) $
     unless (binderInfos.get! i).isInstImplicit $ do
       currTag ← getMVarTag newMVarId;
-      renameMVar newMVarId (parentTag ++ currTag.eraseMacroScopes)
+      setMVarTag newMVarId (appendTag parentTag currTag)
 
 def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
 synthAppInstances tacticName mvarId newMVars binderInfos;

src/Lean/Meta/Tactic/Util.lean

@@ -18,9 +18,14 @@ pure mvarDecl.userName
 def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
 modify $ fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag }
 
+def appendTag (tag : Name) (suffix : Name) : Name :=
+let view := extractMacroScopes tag;
+let view := { view with name := view.name ++ suffix.eraseMacroScopes };
+view.review
+
 def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do
 tag ← getMVarTag mvarId;
-setMVarTag mvarId (tag ++ suffix)
+setMVarTag mvarId (appendTag tag suffix)
 
 def mkFreshExprSyntheticOpaqueMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr :=
 mkFreshExprMVar type MetavarKind.syntheticOpaque userName

src/Lean/Util/PPGoal.lean

@@ -51,6 +51,6 @@ match mctx.findDecl? mvarId with
   let fmt := fmt ++ "⊢" ++ " " ++ Format.nest indent (pp mvarDecl.type);
   match mvarDecl.userName with
   | Name.anonymous => fmt
-  | name           => "case " ++ format name ++ Format.line ++ fmt
+  | name           => "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
 
 end Lean