diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index a1de10d2b6..f5d603fcde 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -353,7 +353,7 @@ def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Exp
     if us == us' then
       return r
   unless c.hasValue do
-    throwError "Not a definition or theorem: {c.name}"
+    throwError "Not a definition or theorem: {.ofConstName c.name}"
   let r := c.instantiateValueLevelParams! us
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index e172b9ac18..f0badc021c 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -119,7 +119,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "beq" declName
+  let ctx ← mkContext ``BEq "beq" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName])
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
@@ -129,7 +129,7 @@ private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   `(def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.ctorIdx == y.ctorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
-  let ctx ← mkContext "beq" name
+  let ctx ← mkContext ``BEq "beq" name
   let cmds := #[← mkBEqEnumFun ctx name] ++ (← mkInstanceCmds ctx `BEq #[name])
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 5b4a443d78..dfb2f5fc0f 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -194,7 +194,7 @@ def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do
   `(command| mutual $[$res:command]* end)
 
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "decEq" indVal.name
+  let ctx ← mkContext ``DecidableEq "decEq" indVal.name
   let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false))
   trace[Elab.Deriving.decEq] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 0c8e51e71e..9160e25e08 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -215,13 +215,13 @@ def mkFromJsonMutualBlock (ctx : Context) : TermElabM Command := do
     end)
 
 private def mkToJsonInstance (declName : Name) : TermElabM (Array Command) := do
-  let ctx ← mkContext "toJson" declName
+  let ctx ← mkContext ``ToJson "toJson" declName
   let cmds := #[← mkToJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``ToJson #[declName])
   trace[Elab.Deriving.toJson] "\n{cmds}"
   return cmds
 
 private def mkFromJsonInstance (declName : Name) : TermElabM (Array Command) := do
-  let ctx ← mkContext "fromJson" declName
+  let ctx ← mkContext ``FromJson "fromJson" declName
   let cmds := #[← mkFromJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``FromJson #[declName])
   trace[Elab.Deriving.fromJson] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index 9ddc3eca29..77932d73a9 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -81,7 +81,7 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
   `(mutual $auxDefs:command* end)
 
 private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "hash" declName
+  let ctx ← mkContext ``Hashable "hash" declName
   let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName])
   trace[Elab.Deriving.hashable] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index b34c46ecaf..a8244b9a68 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -61,7 +61,7 @@ where
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
      at position `i` and `i ∈ assumingParamIdxs`. -/
   mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
-    let ctx ← Deriving.mkContext "inhabited" inductiveTypeName
+    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
     let indVal ← getConstInfoInduct inductiveTypeName
     let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
@@ -81,7 +81,7 @@ where
     for _ in *...ctorVal.numFields do
       ctorArgs := ctorArgs.push (← ``(Inhabited.default))
     let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
-    let ctx ← mkContext "default" inductiveTypeName
+    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
     let auxFunName := ctx.auxFunNames[0]!
     `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
       instance $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index c3d73545d9..a72eeeba0c 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -90,7 +90,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkOrdInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "ord" declName
+  let ctx ← mkContext ``Ord "ord" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord #[declName])
   trace[Elab.Deriving.ord] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 977382bf6d..92065c3c4b 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -114,7 +114,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "repr" declName
+  let ctx ← mkContext ``Repr "repr" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName])
   trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
index c9e9e9a173..0a7aff9f7b 100644
--- a/src/Lean/Elab/Deriving/ToExpr.lean
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -216,7 +216,7 @@ def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
 Returns all the commands necessary to construct the `ToExpr` instances.
 -/
 def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "toExpr" declNames[0]!
+  let ctx ← mkContext ``ToExpr "toExpr" declNames[0]!
   let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx declNames)
   trace[Elab.Deriving.toExpr] "\n{cmds}"
   return cmds
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index 07bf869628..55832e2593 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Term
 public import Lean.Elab.Command
 meta import Lean.Parser.Command
+import Lean.Elab.DeclNameGen
 
 public section
 
@@ -84,23 +85,33 @@ def withoutExposeFromCtors (typeName : Name) (cont : CommandElabM α) : CommandE
   else cont
 
 structure Context where
+  instName    : Name
   typeInfos   : Array InductiveVal
   auxFunNames : Array Name
   usePartial  : Bool
 
-def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
+
+def mkContext (className : Name) (fnPrefix : String) (typeName : Name) : TermElabM Context := do
   let indVal ← getConstInfoInduct typeName
   let mut typeInfos := #[]
   for typeName in indVal.all do
     typeInfos := typeInfos.push (← getConstInfoInduct typeName)
+  let instName ← do -- anticipate the instance name
+    let argNames     ← mkInductArgNames indVal
+    let binders      ← mkImplicitBinders argNames
+    let indType      ← mkInductiveApp indVal argNames
+    let type         ← `($(mkCIdent className) $indType)
+    NameGen.mkBaseNameWithSuffix' "inst" (binders.map (·.raw)) type
   let mut auxFunNames := #[]
-  for typeName in indVal.all do
-    match typeName.eraseMacroScopes with
-    | .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
-    | _        => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
-  trace[Elab.Deriving.beq] "{auxFunNames}"
+  if indVal.all.length = 1 then
+    auxFunNames := auxFunNames.push (instName ++ .mkSimple fnPrefix)
+  else
+    for i in [:indVal.all.length] do
+      auxFunNames := auxFunNames.push (instName ++ .mkSimple s!"{fnPrefix}_{i+1}")
+  trace[Elab.Deriving] "instName: {instName} auxFunNames: {auxFunNames}"
   let usePartial := indVal.isNested || typeInfos.size > 1
   return {
+    instName    := instName
     typeInfos   := typeInfos
     auxFunNames := auxFunNames
     usePartial  := usePartial
@@ -143,7 +154,7 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let mut val      := mkIdent auxFunName
       if useAnonCtor then
         val ← `(⟨$val⟩)
-      let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
+      let instCmd ← `(instance $(mkIdent ctx.instName):ident $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
 
diff --git a/tests/lean/decEqMutualInductives.lean.expected.out b/tests/lean/decEqMutualInductives.lean.expected.out
index d8d0ec512e..0d92e3d9fe 100644
--- a/tests/lean/decEqMutualInductives.lean.expected.out
+++ b/tests/lean/decEqMutualInductives.lean.expected.out
@@ -1,108 +1,108 @@
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqTree✝ (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqListTree.decEq_1 (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @A.Tree.node a✝, @A.Tree.node b✝ =>
-           let inst✝ := decEqListTree✝ @a✝ @b✝;
+           let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝;
            if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
            else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        termination_by structural x✝
-       def decEqListTree✝ (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqListTree.decEq_2 (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @A.ListTree.nil, @A.ListTree.nil => isTrue✝¹ rfl✝¹
          | A.ListTree.nil .., A.ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | A.ListTree.cons .., A.ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | @A.ListTree.cons a✝¹ a✝², @A.ListTree.cons b✝¹ b✝² =>
-           let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
+           let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹;
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
              exact
-               let inst✝² := decEqListTree✝ @a✝² @b✝²;
+               let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²;
                if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
        termination_by structural x✝²
      end,
-     instance : DecidableEq✝ (@A.ListTree✝) :=
-       decEqListTree✝]
+     instance instDecidableEqListTree : DecidableEq✝ (@A.ListTree✝) :=
+       instDecidableEqListTree.decEq_2]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqFoo₁✝ (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqFoo₁.decEq_1 (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @A.Foo₁.foo₁₁, @A.Foo₁.foo₁₁ => isTrue✝ rfl✝
          | A.Foo₁.foo₁₁ .., A.Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝)
          | A.Foo₁.foo₁₂ .., A.Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝)
          | @A.Foo₁.foo₁₂ a✝, @A.Foo₁.foo₁₂ b✝ =>
-           let inst✝ := decEqFoo₂✝ @a✝ @b✝;
+           let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝;
            if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
            else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
        termination_by structural x✝
-       def decEqFoo₂✝ (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqFoo₁.decEq_2 (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @A.Foo₂.foo₂ a✝¹, @A.Foo₂.foo₂ b✝¹ =>
-           let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
+           let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹;
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
            else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        termination_by structural x✝²
-       def decEqFoo₃✝ (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
+       def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          match x✝⁴, x✝⁵ with
          | @A.Foo₃.foo₃ a✝², @A.Foo₃.foo₃ b✝² =>
-           let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
+           let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²;
            if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
        termination_by structural x✝⁴
      end,
-     instance : DecidableEq✝ (@A.Foo₁✝) :=
-       decEqFoo₁✝]
+     instance instDecidableEqFoo₁ : DecidableEq✝ (@A.Foo₁✝) :=
+       instDecidableEqFoo₁.decEq_1]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqTree✝ (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqListTree.decEq_1 (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          B.Tree.match_on_same_ctor✝ x✝ x✝¹ rfl✝
            @fun a✝ b✝ =>
-             let inst✝ := decEqListTree✝ @a✝ @b✝;
+             let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝;
              if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝¹
              else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        termination_by structural x✝
-       def decEqListTree✝ (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqListTree.decEq_2 (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          if h✝¹ : B.ListTree.ctorIdx✝ x✝² = B.ListTree.ctorIdx✝ x✝³ then
            B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun => isTrue✝¹ rfl✝)
              @fun a✝¹ a✝² b✝¹ b✝² =>
-               let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
+               let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹;
                if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
                  exact
-                   let inst✝² := decEqListTree✝ @a✝² @b✝²;
+                   let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²;
                    if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                    else isFalse✝¹ (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
                else isFalse✝² (by intro n✝²; injection n✝²; apply h✝² _; assumption)
          else isFalse✝³ (fun h'✝ => h✝¹ (congrArg✝ B.ListTree.ctorIdx✝ h'✝))
        termination_by structural x✝²
      end,
-     instance : DecidableEq✝ (@B.ListTree✝) :=
-       decEqListTree✝]
+     instance instDecidableEqListTree : DecidableEq✝ (@B.ListTree✝) :=
+       instDecidableEqListTree.decEq_2]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqFoo₁✝ (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqFoo₁.decEq_1 (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
          if h✝ : B.Foo₁.ctorIdx✝ x✝ = B.Foo₁.ctorIdx✝ x✝¹ then
            B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun => isTrue✝ rfl✝)
              @fun a✝ b✝ =>
-               let inst✝ := decEqFoo₂✝ @a✝ @b✝;
+               let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝;
                if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
                else isFalse✝ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
          else isFalse✝¹ (fun h'✝ => h✝ (congrArg✝ B.Foo₁.ctorIdx✝ h'✝))
        termination_by structural x✝
-       def decEqFoo₂✝ (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqFoo₁.decEq_2 (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          B.Foo₂.match_on_same_ctor✝ x✝² x✝³ rfl✝
            @fun a✝¹ b✝¹ =>
-             let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
+             let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹;
              if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
              else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        termination_by structural x✝²
-       def decEqFoo₃✝ (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
+       def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          B.Foo₃.match_on_same_ctor✝ x✝⁴ x✝⁵ rfl✝
            @fun a✝² b✝² =>
-             let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
+             let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²;
              if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
              else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
        termination_by structural x✝⁴
      end,
-     instance : DecidableEq✝ (@B.Foo₁✝) :=
-       decEqFoo₁✝]
+     instance instDecidableEqFoo₁ : DecidableEq✝ (@B.Foo₁✝) :=
+       instDecidableEqFoo₁.decEq_1]
diff --git a/tests/lean/prvNameWithMacroScopes.lean b/tests/lean/prvNameWithMacroScopes.lean
deleted file mode 100644
index cd97591112..0000000000
--- a/tests/lean/prvNameWithMacroScopes.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Lean
-#print Lean.instBEqFVarId
diff --git a/tests/lean/prvNameWithMacroScopes.lean.expected.out b/tests/lean/prvNameWithMacroScopes.lean.expected.out
deleted file mode 100644
index b19042cbc9..0000000000
--- a/tests/lean/prvNameWithMacroScopes.lean.expected.out
+++ /dev/null
@@ -1,2 +0,0 @@
-def Lean.instBEqFVarId : BEq Lean.FVarId :=
-{ beq := Lean.beqFVarId✝ }
diff --git a/tests/lean/run/2161.lean b/tests/lean/run/2161.lean
index afa0b3f39d..4d2ebe6398 100644
--- a/tests/lean/run/2161.lean
+++ b/tests/lean/run/2161.lean
@@ -19,7 +19,7 @@ because its `Decidable` instance
   instDecidableEqFoo (((mul 4 1).mul 1).mul 1) 4
 did not reduce to `isTrue` or `isFalse`.
 
-After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance
+After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance
   match h : (((mul 4 1).mul 1).mul 1).num.beq 4 with
   | true => isTrue ⋯
   | false => isFalse ⋯
@@ -39,7 +39,7 @@ because its `Decidable` instance
   instDecidableEqFoo (((add 4 1).add 1).add 1) 4
 did not reduce to `isTrue` or `isFalse`.
 
-After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance
+After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance
   match h : (((add 4 1).add 1).add 1).num.beq 4 with
   | true => isTrue ⋯
   | false => isFalse ⋯
diff --git a/tests/lean/run/decEq.lean b/tests/lean/run/decEq.lean
index f7a97bd928..05f91add92 100644
--- a/tests/lean/run/decEq.lean
+++ b/tests/lean/run/decEq.lean
@@ -32,7 +32,9 @@ public inductive PubInd where
   | a (n : Nat) | b
 deriving DecidableEq
 
-/-- info: Decidable.rec (fun h => false) (fun h => true) (decEqPubInd✝ PubInd.b PubInd.b) -/
+/--
+info: Decidable.rec (fun h => false) (fun h => true) (instDecidableEqPubInd.decEq PubInd.b PubInd.b)
+-/
 #guard_msgs in
 #with_exporting
 #reduce decide (PubInd.b = PubInd.b)
diff --git a/tests/lean/run/derivingBEq.lean b/tests/lean/run/derivingBEq.lean
index bd9c8408c3..9db179cb06 100644
--- a/tests/lean/run/derivingBEq.lean
+++ b/tests/lean/run/derivingBEq.lean
@@ -75,7 +75,7 @@ structure PrivField where
   private a : Nat
 deriving BEq
 
-/-- info: fun a => beqPrivField✝ a a -/
+/-- info: fun a => instBEqPrivField.beq a a -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField) => a == a
@@ -88,7 +88,7 @@ public structure PrivField2 where
   private a : Nat
 deriving BEq
 
-/-- info: fun a => beqPrivField2✝ a a -/
+/-- info: fun a => instBEqPrivField2.beq a a -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField2) => a == a
diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean
index 156eb68f80..32dbfdf477 100644
--- a/tests/lean/run/derivingInhabited.lean
+++ b/tests/lean/run/derivingInhabited.lean
@@ -55,7 +55,7 @@ deriving Inhabited
 
 /--
 info: private def instInhabitedA : Inhabited A :=
-{ default := defaultA✝ }
+{ default := instInhabitedA.default }
 -/
 #guard_msgs in
 #print instInhabitedA
@@ -66,7 +66,7 @@ public structure PrivField where
   private a : Nat
 deriving Inhabited
 
-/-- info: defaultPrivField✝ -/
+/-- info: instInhabitedPrivField.default -/
 #guard_msgs in
 #with_exporting
 #reduce (default : PrivField)
diff --git a/tests/lean/run/derivingRepr.lean b/tests/lean/run/derivingRepr.lean
index 726c602d4d..93848eb577 100644
--- a/tests/lean/run/derivingRepr.lean
+++ b/tests/lean/run/derivingRepr.lean
@@ -122,7 +122,7 @@ structure PrivField where
   private a : Nat
 deriving Repr
 
-/-- info: fun a => reprPrivField✝ a 0 -/
+/-- info: fun a => instReprPrivField.repr a 0 -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField) => repr a
@@ -135,7 +135,7 @@ public structure PrivField2 where
   private a : Nat
 deriving Repr
 
-/-- info: fun a => reprPrivField2✝ a 0 -/
+/-- info: fun a => instReprPrivField2.repr a 0 -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField2) => repr a
@@ -147,7 +147,7 @@ deriving Repr
 
 /--
 info: @[expose] def instReprPublic : Repr Public :=
-{ reprPrec := reprPublic✝ }
+{ reprPrec := instReprPublic.repr }
 -/
 #guard_msgs in
 #with_exporting
diff --git a/tests/lean/run/prvNameWithMacroScopes.lean b/tests/lean/run/prvNameWithMacroScopes.lean
new file mode 100644
index 0000000000..99fbf895ef
--- /dev/null
+++ b/tests/lean/run/prvNameWithMacroScopes.lean
@@ -0,0 +1,13 @@
+macro "test%" n:ident : command =>
+  `(def foo := 42
+    def $n := foo
+  )
+
+test% bar
+
+/--
+info: def bar : Nat :=
+foo✝
+-/
+#guard_msgs in
+#print bar