diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 8a308c7b66..33ae8ec5e3 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1215,7 +1215,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let fullName := Name.mkStr structName fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
-        if let some localDeclFullName := (← read).auxDeclToFullName.find? localDecl.fvarId then
+        if let some localDeclFullName := (← getLCtx).auxDeclToFullName.find? localDecl.fvarId then
           if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName fullName localDecl.toExpr
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 1ec31cf65e..63ff3f75e5 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -336,7 +336,7 @@ private def withInductiveLocalDecls (rs : Array PreElabHeaderResult) (x : Array
     let rec loop (i : Nat) (indFVars : Array Expr) := do
       if h : i < namesAndTypes.size then
         let (declName, shortDeclName, type) := namesAndTypes[i]
-        Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
+        withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars
     loop 0 #[]
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 55c381a9da..725371475c 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -258,10 +258,6 @@ namespace Term
 
 structure Context where
   declName? : Option Name := none
-  /--
-    Map `.auxDecl` local declarations used to encode recursive declarations to their full-names.
-  -/
-  auxDeclToFullName : FVarIdMap Name  := {}
   macroStack        : MacroStack      := []
   /--
      When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
@@ -627,15 +623,6 @@ def withLevelNames (levelNames : List Name) (x : TermElabM α) : TermElabM α :=
   setLevelNames levelNames
   try x finally setLevelNames levelNamesSaved
 
-/--
-  Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive declaration `declName`,
-  update the mapping `auxDeclToFullName`, and then execute `k`.
--/
-def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → TermElabM α) : TermElabM α :=
-  withLocalDecl shortDeclName .default (kind := .auxDecl) type fun x =>
-    withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
-      k x
-
 def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
   withReader (fun ctx => { ctx with errToSorry := false }) x
 
@@ -1522,169 +1509,6 @@ def blockImplicitLambda (stx : Syntax) : Bool :=
   isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx ||
   isNoImplicitLambda stx || isTypeAscription stx
 
-def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
-  let lctx ← getLCtx
-  let auxDeclToFullName := (← read).auxDeclToFullName
-  let currNamespace ← getCurrNamespace
-  let view := extractMacroScopes n
-  /- Simple case. "Match" function for regular local declarations. -/
-  let matchLocalDecl? (localDecl : LocalDecl) (givenName : Name) : Option LocalDecl := do
-    guard (localDecl.userName == givenName)
-    return localDecl
-  /-
-  "Match" function for auxiliary declarations that correspond to recursive definitions being defined.
-  This function is used in the first-pass.
-  Note that we do not check for `localDecl.userName == givenName` in this pass as we do for regular local declarations.
-  Reason: consider the following example
-  ```
-    mutual
-      inductive Foo
-      | somefoo : Foo | bar : Bar → Foo → Foo
-      inductive Bar
-      | somebar : Bar| foobar : Foo → Bar → Bar
-    end
-
-    mutual
-      private def Foo.toString : Foo → String
-        | Foo.somefoo => go 2 ++ toString.go 2 ++ Foo.toString.go 2
-        | Foo.bar b f => toString f ++ Bar.toString b
-      where
-        go (x : Nat) := s!"foo {x}"
-
-      private def _root_.Ex2.Bar.toString : Bar → String
-        | Bar.somebar => "bar"
-        | Bar.foobar f b => Foo.toString f ++ Bar.toString b
-    end
-  ```
-  In the example above, we have two local declarations named `toString` in the local context, and
-  we want the `toString f` to be resolved to `Foo.toString f`.
-  -/
-  let matchAuxRecDecl? (localDecl : LocalDecl) (fullDeclName : Name) (givenNameView : MacroScopesView) : Option LocalDecl := do
-    let fullDeclView := extractMacroScopes fullDeclName
-    /- First cleanup private name annotations -/
-    let fullDeclView := { fullDeclView with name := (privateToUserName? fullDeclView.name).getD fullDeclView.name }
-    let fullDeclName := fullDeclView.review
-    let localDeclNameView := extractMacroScopes localDecl.userName
-    /- If the current namespace is a prefix of the full declaration name,
-       we use a relaxed matching test where we must satisfy the following conditions
-       - The local declaration is a suffix of the given name.
-       - The given name is a suffix of the full declaration.
-
-       Recall the `let rec`/`where` declaration naming convention. For example, suppose we have
-       ```
-       def Foo.Bla.f ... :=
-         ... go ...
-       where
-          go ... := ...
-       ```
-       The current namespace is `Foo.Bla`, and the full name for `go` is `Foo.Bla.f.g`, but we want to
-       refer to it using just `go`. It is also accepted to refer to it using `f.go`, `Bla.f.go`, etc.
-
-    -/
-    if currNamespace.isPrefixOf fullDeclName then
-      /- Relaxed mode that allows us to access `let rec` declarations using shorter names -/
-      guard (localDeclNameView.isSuffixOf givenNameView)
-      guard (givenNameView.isSuffixOf fullDeclView)
-      return localDecl
-    else
-      /-
-         It is the standard algorithm we are using at `resolveGlobalName` for processing namespaces.
-
-         The current solution also has a limitation when using `def _root_` in a mutual block.
-         The non `def _root_` declarations may update the namespace. See the following example:
-         ```
-         mutual
-           def Foo.f ... := ...
-           def _root_.g ... := ...
-             let rec h := ...
-             ...
-         end
-         ```
-         `def Foo.f` updates the namespace. Then, even when processing `def _root_.g ...`
-         the condition `currNamespace.isPrefixOf fullDeclName` does not hold.
-         This is not a big problem because we are planning to modify how we handle the mutual block in the future.
-
-         Note that we don't check for `localDecl.userName == givenName` here.
-      -/
-      let rec go (ns : Name) : Option LocalDecl := do
-        if { givenNameView with name := ns ++ givenNameView.name }.review == fullDeclName then
-          return localDecl
-        match ns with
-        | .str pre .. => go pre
-        | _ => failure
-      return (← go currNamespace)
-  /- Traverse the local context backwards looking for match `givenNameView`.
-     If `skipAuxDecl` we ignore `auxDecl` local declarations. -/
-  let findLocalDecl? (givenNameView : MacroScopesView) (skipAuxDecl : Bool) : Option LocalDecl :=
-    let givenName := givenNameView.review
-    let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
-      let localDecl ← localDecl?
-      if localDecl.isAuxDecl then
-        guard (!skipAuxDecl)
-        if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
-          matchAuxRecDecl? localDecl fullDeclName givenNameView
-        else
-          matchLocalDecl? localDecl givenName
-      else
-        matchLocalDecl? localDecl givenName
-    if localDecl?.isSome || skipAuxDecl then
-      localDecl?
-    else
-      -- Search auxDecls again trying an exact match of the given name
-      lctx.decls.findSomeRev? fun localDecl? => do
-        let localDecl ← localDecl?
-        guard localDecl.isAuxDecl
-        matchLocalDecl? localDecl givenName
-  /-
-  We use the parameter `globalDeclFound` to decide whether we should skip auxiliary declarations or not.
-  We set it to true if we found a global declaration `n` as we iterate over the `loop`.
-  Without this workaround, we would not be able to elaborate an example such as
-  ```
-  def foo.aux := 1
-  def foo : Nat → Nat
-    | n => foo.aux -- should not be interpreted as `(foo).aux`
-  ```
-  See test `aStructPerfIssue.lean` for another example.
-  We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
-  Remark: we did not use to have the `globalDeclFound` parameter. Without this extra check we failed
-  to elaborate
-  ```
-  example : Nat :=
-    let n := 0
-    n.succ + (m |>.succ) + m.succ
-  where
-    m := 1
-  ```
-  See issue #1850.
-  -/
-  let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
-    let givenNameView := { view with name := n }
-    let mut globalDeclFoundNext := globalDeclFound
-    unless globalDeclFound do
-      let r ← resolveGlobalName givenNameView.review
-      let r := r.filter fun (_, fieldList) => fieldList.isEmpty
-      unless r.isEmpty do
-        globalDeclFoundNext := true
-    /-
-    Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
-    Reason: a local should shadow a global with the same name.
-    Consider the following example. See issue #3079
-    ```
-    def foo : Nat := 1
-
-    def bar : Nat :=
-      foo.add 1 -- should be 11
-    where
-      foo := 10
-    ```
-    -/
-    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
-    | some decl => return some (decl.toExpr, projs)
-    | none => match n with
-      | .str pre s => loop pre (s::projs) globalDeclFoundNext
-      | _ => return none
-  loop view.name [] (globalDeclFound := false)
-
 /-- Return true iff `stx` is a `Syntax.ident`, and it is a local variable. -/
 def isLocalIdent? (stx : Syntax) : TermElabM (Option Expr) :=
   match stx with
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 3ff45c2ffa..f946726d33 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -159,14 +159,16 @@ end LocalDecl
 
 /-- A LocalContext is an ordered set of local variable declarations.
 It is used to store the free variables (also known as local constants) that
-are in scope.
+are in scope. It also maps free variables corresponding to auxiliary declarations
+(recursive references and `where` and `let rec` bindings) to their fully-qualified global names.
 
 When inspecting a goal or expected type in the infoview, the local
 context is all of the variables above the `⊢` symbol.
  -/
 structure LocalContext where
-  fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {}
-  decls        : PersistentArray (Option LocalDecl) := {}
+  fvarIdToDecl      : PersistentHashMap FVarId LocalDecl := {}
+  decls             : PersistentArray (Option LocalDecl) := {}
+  auxDeclToFullName : FVarIdMap Name                     := {}
   deriving Inhabited
 
 namespace LocalContext
@@ -186,10 +188,10 @@ It should not be used directly since the argument `(fvarId : FVarId)` is
 assumed to be unique. You can create a unique fvarId with `mkFreshFVarId`. -/
 def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := .default) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     let idx  := decls.size
     let decl := LocalDecl.cdecl idx fvarId userName type bi kind
-    { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
+    { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
 
 -- `mkLocalDecl` without `kind`
 @[export lean_local_ctx_mk_local_decl]
@@ -199,23 +201,34 @@ private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userNam
 /-- Low level API for let declarations. Do not use directly.-/
 def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) (kind : LocalDeclKind := default) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     let idx  := decls.size
     let decl := LocalDecl.ldecl idx fvarId userName type value nonDep kind
-    { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
+    { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
 
 @[export lean_local_ctx_mk_let_decl]
 private def mkLetDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) : LocalContext :=
   mkLetDecl lctx fvarId userName type value nonDep
 
+/-- Low level API for auxiliary declarations. Do not use directly. -/
+def mkAuxDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (fullName : Name) : LocalContext :=
+  match lctx with
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
+    let idx  := decls.size
+    let decl := LocalDecl.cdecl idx fvarId userName type .default .auxDecl
+    let auxDeclToFullName := auxDeclToFullName.insert fvarId fullName
+    { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
+
 /-- Low level API for adding a local declaration.
 Do not use directly. -/
 def addDecl (lctx : LocalContext) (newDecl : LocalDecl) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     let idx     := decls.size
     let newDecl := newDecl.setIndex idx
-    { fvarIdToDecl := map.insert newDecl.fvarId newDecl, decls := decls.push newDecl }
+    { fvarIdToDecl := map.insert newDecl.fvarId newDecl
+      decls        := decls.push newDecl
+      auxDeclToFullName }
 
 @[export lean_local_ctx_find]
 def find? (lctx : LocalContext) (fvarId : FVarId) : Option LocalDecl :=
@@ -260,18 +273,26 @@ private partial def popTailNoneAux (a : PArray (Option LocalDecl)) : PArray (Opt
 @[export lean_local_ctx_erase]
 def erase (lctx : LocalContext) (fvarId : FVarId) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     match map.find? fvarId with
     | none      => lctx
-    | some decl => { fvarIdToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
+    | some decl =>
+      { fvarIdToDecl      := map.erase fvarId
+        decls             := popTailNoneAux (decls.set decl.index none)
+        auxDeclToFullName :=
+          if decl.isAuxDecl then auxDeclToFullName.erase fvarId else auxDeclToFullName }
 
-def pop (lctx : LocalContext): LocalContext :=
+def pop (lctx : LocalContext) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     if _ : decls.size = 0 then lctx
     else match decls[decls.size - 1] with
       | none      => lctx -- unreachable
-      | some decl => { fvarIdToDecl := map.erase decl.fvarId, decls := popTailNoneAux decls.pop }
+      | some decl =>
+        { fvarIdToDecl      := map.erase decl.fvarId
+          decls             := popTailNoneAux decls.pop
+          auxDeclToFullName :=
+            if decl.isAuxDecl then auxDeclToFullName.erase decl.fvarId else auxDeclToFullName }
 
 def findFromUserName? (lctx : LocalContext) (userName : Name) : Option LocalDecl :=
   lctx.decls.findSomeRev? fun decl =>
@@ -298,18 +319,20 @@ def lastDecl (lctx : LocalContext) : Option LocalDecl :=
 def setUserName (lctx : LocalContext) (fvarId : FVarId) (userName : Name) : LocalContext :=
   let decl := lctx.get! fvarId
   let decl := decl.setUserName userName
-  { fvarIdToDecl := lctx.fvarIdToDecl.insert decl.fvarId decl,
-    decls        := lctx.decls.set decl.index decl }
+  { fvarIdToDecl      := lctx.fvarIdToDecl.insert decl.fvarId decl,
+    decls             := lctx.decls.set decl.index decl,
+    auxDeclToFullName := lctx.auxDeclToFullName }
 
 def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     match lctx.findFromUserName? fromName with
     | none      => lctx
     | some decl =>
       let decl := decl.setUserName toName;
       { fvarIdToDecl := map.insert decl.fvarId decl,
-        decls        := decls.set decl.index decl }
+        decls        := decls.set decl.index decl,
+        auxDeclToFullName }
 
 /--
   Low-level function for updating the local context.
@@ -317,13 +340,14 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
   the `index` nor `fvarId` are modified.  -/
 @[inline] def modifyLocalDecl (lctx : LocalContext) (fvarId : FVarId) (f : LocalDecl → LocalDecl) : LocalContext :=
   match lctx with
-  | { fvarIdToDecl := map, decls := decls } =>
+  | { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
     match lctx.find? fvarId with
     | none      => lctx
     | some decl =>
       let decl := f decl
       { fvarIdToDecl := map.insert decl.fvarId decl
-        decls        := decls.set decl.index decl }
+        decls        := decls.set decl.index decl
+        auxDeclToFullName }
 
 /--
 Set the kind of the given fvar.
@@ -520,6 +544,7 @@ def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : Local
 def LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext :=
   let lctx := lctx.erase fvarId
   { fvarIdToDecl := lctx.fvarIdToDecl.map (·.replaceFVarId fvarId e)
-    decls := lctx.decls.map fun localDecl? => localDecl?.map (·.replaceFVarId fvarId e) }
+    decls := lctx.decls.map fun localDecl? => localDecl?.map (·.replaceFVarId fvarId e),
+    auxDeclToFullName := lctx.auxDeclToFullName }
 
 end Lean
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 689c71c8ae..ac4c147777 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1664,6 +1664,21 @@ def withLocalDeclsDND [Inhabited α] (declInfos : Array (Name × Expr)) (k : (xs
   withLocalDeclsD
     (declInfos.map (fun (name, typeCtor) => (name, fun _ => pure typeCtor))) k
 
+private def withAuxDeclImp (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → MetaM α) : MetaM α := do
+  let fvarId ← mkFreshFVarId
+  let ctx ← read
+  let lctx := ctx.lctx.mkAuxDecl fvarId shortDeclName type declName
+  let fvar := mkFVar fvarId
+  withReader (fun ctx => { ctx with lctx := lctx }) do
+    withNewFVar fvar type k
+
+/--
+  Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive
+  declaration `declName`, update the mapping `auxDeclToFullName`, and then execute `k`.
+-/
+def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → n α) : n α :=
+  map1MetaM (fun k => withAuxDeclImp shortDeclName type declName k) k
+
 private def withNewBinderInfosImp (bs : Array (FVarId × BinderInfo)) (k : MetaM α) : MetaM α := do
   let lctx := bs.foldl (init := (← getLCtx)) fun lctx (fvarId, bi) =>
       lctx.setBinderInfo fvarId bi
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index ee67968d30..efeee7cb27 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -588,8 +588,15 @@ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do
     return r
 
 def instantiateLCtxMVars [Monad m] [MonadMCtx m] (lctx : LocalContext) : m LocalContext :=
+  let auxDeclToFullName := lctx.auxDeclToFullName
   lctx.foldlM (init := {}) fun lctx ldecl => do
      match ldecl with
+     | .cdecl _ fvarId userName type _ .auxDecl =>
+        let type ← instantiateMVars type
+        let .some fullName := auxDeclToFullName.find? fvarId
+          | panic! s!"Invalid auxiliary declaration found in local context: \
+                      {userName} does not have an associated full name."
+        return lctx.mkAuxDecl fvarId userName type fullName
      | .cdecl _ fvarId userName type bi k =>
        let type ← instantiateMVars type
        return lctx.mkLocalDecl fvarId userName type bi k
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index a5167193d9..7c8aa9a276 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -391,6 +391,170 @@ After `open Foo open Boo`, we have
 def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
   ensureNonAmbiguous id (← resolveGlobalConst id)
 
+/-- Resolves the name `n` in the local context. -/
+def resolveLocalName [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n : Name) : m (Option (Expr × List String)) := do
+  let lctx ← getLCtx
+  let auxDeclToFullName := (← getLCtx).auxDeclToFullName
+  let currNamespace ← getCurrNamespace
+  let view := extractMacroScopes n
+  /- Simple case. "Match" function for regular local declarations. -/
+  let matchLocalDecl? (localDecl : LocalDecl) (givenName : Name) : Option LocalDecl := do
+    guard (localDecl.userName == givenName)
+    return localDecl
+  /-
+  "Match" function for auxiliary declarations that correspond to recursive definitions being defined.
+  This function is used in the first-pass.
+  Note that we do not check for `localDecl.userName == givenName` in this pass as we do for regular local declarations.
+  Reason: consider the following example
+  ```
+    mutual
+      inductive Foo
+      | somefoo : Foo | bar : Bar → Foo → Foo
+      inductive Bar
+      | somebar : Bar| foobar : Foo → Bar → Bar
+    end
+
+    mutual
+      private def Foo.toString : Foo → String
+        | Foo.somefoo => go 2 ++ toString.go 2 ++ Foo.toString.go 2
+        | Foo.bar b f => toString f ++ Bar.toString b
+      where
+        go (x : Nat) := s!"foo {x}"
+
+      private def _root_.Ex2.Bar.toString : Bar → String
+        | Bar.somebar => "bar"
+        | Bar.foobar f b => Foo.toString f ++ Bar.toString b
+    end
+  ```
+  In the example above, we have two local declarations named `toString` in the local context, and
+  we want the `toString f` to be resolved to `Foo.toString f`.
+  -/
+  let matchAuxRecDecl? (localDecl : LocalDecl) (fullDeclName : Name) (givenNameView : MacroScopesView) : Option LocalDecl := do
+    let fullDeclView := extractMacroScopes fullDeclName
+    /- First cleanup private name annotations -/
+    let fullDeclView := { fullDeclView with name := (privateToUserName? fullDeclView.name).getD fullDeclView.name }
+    let fullDeclName := fullDeclView.review
+    let localDeclNameView := extractMacroScopes localDecl.userName
+    /- If the current namespace is a prefix of the full declaration name,
+       we use a relaxed matching test where we must satisfy the following conditions
+       - The local declaration is a suffix of the given name.
+       - The given name is a suffix of the full declaration.
+
+       Recall the `let rec`/`where` declaration naming convention. For example, suppose we have
+       ```
+       def Foo.Bla.f ... :=
+         ... go ...
+       where
+          go ... := ...
+       ```
+       The current namespace is `Foo.Bla`, and the full name for `go` is `Foo.Bla.f.g`, but we want to
+       refer to it using just `go`. It is also accepted to refer to it using `f.go`, `Bla.f.go`, etc.
+
+    -/
+    if currNamespace.isPrefixOf fullDeclName then
+      /- Relaxed mode that allows us to access `let rec` declarations using shorter names -/
+      guard (localDeclNameView.isSuffixOf givenNameView)
+      guard (givenNameView.isSuffixOf fullDeclView)
+      return localDecl
+    else
+      /-
+         It is the standard algorithm we are using at `resolveGlobalName` for processing namespaces.
+
+         The current solution also has a limitation when using `def _root_` in a mutual block.
+         The non `def _root_` declarations may update the namespace. See the following example:
+         ```
+         mutual
+           def Foo.f ... := ...
+           def _root_.g ... := ...
+             let rec h := ...
+             ...
+         end
+         ```
+         `def Foo.f` updates the namespace. Then, even when processing `def _root_.g ...`
+         the condition `currNamespace.isPrefixOf fullDeclName` does not hold.
+         This is not a big problem because we are planning to modify how we handle the mutual block in the future.
+
+         Note that we don't check for `localDecl.userName == givenName` here.
+      -/
+      let rec go (ns : Name) : Option LocalDecl := do
+        if { givenNameView with name := ns ++ givenNameView.name }.review == fullDeclName then
+          return localDecl
+        match ns with
+        | .str pre .. => go pre
+        | _ => failure
+      return (← go currNamespace)
+  /- Traverse the local context backwards looking for match `givenNameView`.
+     If `skipAuxDecl` we ignore `auxDecl` local declarations. -/
+  let findLocalDecl? (givenNameView : MacroScopesView) (skipAuxDecl : Bool) : Option LocalDecl :=
+    let givenName := givenNameView.review
+    let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
+      let localDecl ← localDecl?
+      if localDecl.isAuxDecl then
+        guard (!skipAuxDecl)
+        if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
+          matchAuxRecDecl? localDecl fullDeclName givenNameView
+        else
+          matchLocalDecl? localDecl givenName
+      else
+        matchLocalDecl? localDecl givenName
+    if localDecl?.isSome || skipAuxDecl then
+      localDecl?
+    else
+      -- Search auxDecls again trying an exact match of the given name
+      lctx.decls.findSomeRev? fun localDecl? => do
+        let localDecl ← localDecl?
+        guard localDecl.isAuxDecl
+        matchLocalDecl? localDecl givenName
+  /-
+  We use the parameter `globalDeclFound` to decide whether we should skip auxiliary declarations or not.
+  We set it to true if we found a global declaration `n` as we iterate over the `loop`.
+  Without this workaround, we would not be able to elaborate an example such as
+  ```
+  def foo.aux := 1
+  def foo : Nat → Nat
+    | n => foo.aux -- should not be interpreted as `(foo).aux`
+  ```
+  See test `aStructPerfIssue.lean` for another example.
+  We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
+  Remark: we did not use to have the `globalDeclFound` parameter. Without this extra check we failed
+  to elaborate
+  ```
+  example : Nat :=
+    let n := 0
+    n.succ + (m |>.succ) + m.succ
+  where
+    m := 1
+  ```
+  See issue #1850.
+  -/
+  let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
+    let givenNameView := { view with name := n }
+    let mut globalDeclFoundNext := globalDeclFound
+    unless globalDeclFound do
+      let r ← resolveGlobalName givenNameView.review
+      let r := r.filter fun (_, fieldList) => fieldList.isEmpty
+      unless r.isEmpty do
+        globalDeclFoundNext := true
+    /-
+    Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
+    Reason: a local should shadow a global with the same name.
+    Consider the following example. See issue #3079
+    ```
+    def foo : Nat := 1
+
+    def bar : Nat :=
+      foo.add 1 -- should be 11
+    where
+      foo := 10
+    ```
+    -/
+    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
+    | some decl => return some (decl.toExpr, projs)
+    | none => match n with
+      | .str pre s => loop pre (s::projs) globalDeclFoundNext
+      | _ => return none
+  loop view.name [] (globalDeclFound := false)
+
 /--
 Finds a name that unambiguously resolves to the given name `n₀`.
 Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
@@ -402,10 +566,14 @@ When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not
 The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
 "Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
 
+`filter` specifies a predicate that the unresolved name must additionally satisfy.
+
 This function is meant to be used for pretty printing.
 If `n₀` is an accessible name, then the result will be an accessible name.
 -/
-def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m]
+    (n₀ : Name) (fullNames := false) (allowHorizAliases := false)
+    (filter : Name → m Bool := fun _ => pure true) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
@@ -428,18 +596,13 @@ where
       candidate := Name.appendCore cmpt candidate
       if let [(potentialMatch, _)] ← resolveGlobalName candidate then
         if potentialMatch == n₀ then
-          return some candidate
+          if (← filter candidate) then
+            return some candidate
     return none
 
-def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m]
-    (n₀ : Name) (fullNames := false) : m Name := do
-  let mut n ← unresolveNameGlobal n₀ fullNames
-  unless (← getLCtx).usesUserName n do return n
-  -- `n` is also a local declaration
-  if n == n₀ then
-    -- `n` is the fully qualified name. So, we append the `_root_` prefix
-    return `_root_ ++ n
-  else
-    return n₀
+/-- Like `Lean.unresolveNameGlobal`, but also ensures that the unresolved name does not conflict
+with the names of any local declarations. -/
+def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name :=
+  unresolveNameGlobal n₀ (fullNames := fullNames) (filter := fun n => Option.isNone <$> resolveLocalName n)
 
 end Lean
diff --git a/tests/lean/run/6706.lean b/tests/lean/run/6706.lean
new file mode 100644
index 0000000000..24dcfe33e6
--- /dev/null
+++ b/tests/lean/run/6706.lean
@@ -0,0 +1,22 @@
+/-!
+# `simp?`-suggested names conflicting with auxiliary declarations
+
+https://github.com/leanprover/lean4/issues/6706
+
+This test ensures that "unresolved" names provided by `simp?` do not conflict with local auxiliary
+declarations.
+-/
+
+def P := True
+theorem N.A.B : P := trivial
+/-- info: Try this: simp only [N.A.B] -/
+#guard_msgs in
+theorem N.X.A.B : P := by
+  simp? [N.A.B]
+
+/-- info: Try this: simp only [_root_.N.A.B] -/
+#guard_msgs in
+theorem A : P :=
+  let rec N.A.B := ()
+  by simp? [_root_.N.A.B]
+where B := ()
diff --git a/tests/lean/run/7073.lean b/tests/lean/run/7073.lean
new file mode 100644
index 0000000000..b1eee910c3
--- /dev/null
+++ b/tests/lean/run/7073.lean
@@ -0,0 +1,25 @@
+/-!
+# Auxiliary declaration name resolution in tactic blocks
+
+https://github.com/leanprover/lean4/issues/7073
+
+It should be possible to refer to auxiliary declarations by partially- or fully-qualified names
+in tactic blocks.
+-/
+
+theorem A : True ∧ True := by
+  let rec B := trivial
+  exact And.intro A.B A.C
+where C := trivial
+
+namespace M
+
+theorem N : True ∧ True ∧ True :=
+  let rec O := by exact M.N.P
+  by exact ⟨N.O, M.N.O, N.P⟩
+where P := trivial
+
+theorem Q.R : Nat → True
+  | 0 => trivial
+  | 1 => by exact Q.R 0
+  | n + 2 => by exact M.Q.R (n + 1)
diff --git a/tests/lean/run/998.lean b/tests/lean/run/998.lean
index 89ba3044a8..2812f470dd 100644
--- a/tests/lean/run/998.lean
+++ b/tests/lean/run/998.lean
@@ -2,7 +2,7 @@ import Lean
 set_option maxHeartbeats 100000
 attribute [simp] Array.findIdx?.loop
 attribute [simp] Lean.expandExplicitBindersAux.loop
-attribute [simp] Lean.Elab.Term.resolveLocalName.loop
+attribute [simp] Lean.resolveLocalName.loop
 
 
 -- Mathlib