diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index f719ee9a681c..4b751882f770 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
   simp
 
 theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
-    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
+    o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
   subst w
   simp
 
@@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
   cases o <;> simp
 
 theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
-    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
 theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
-    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
 theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 53d48839c935..64b8b9f61141 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -90,6 +90,7 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
+        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
          let value ← elabTermEnsuringType view.valStx type
          mkLambdaFVars xs value
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 13802a58f901..d37aa7381743 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -410,11 +410,15 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-          -- synthesize mvars here to force the top-level tactic block (if any) to run
-          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-        -- leads to more section variables being included than necessary
-        let val ← instantiateMVarsProfiling val
+          -- Store instantiated body in info tree for the benefit of the unused variables linter
+          -- and other metaprograms that may want to inspect it without paying for the instantiation
+          -- again
+          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
+            -- synthesize mvars here to force the top-level tactic block (if any) to run
+            let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+            -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+            -- leads to more section variables being included than necessary
+            instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do
diff --git a/src/Lean/Linter/ConstructorAsVariable.lean b/src/Lean/Linter/ConstructorAsVariable.lean
index 1c9229830efb..3a063b36c769 100644
--- a/src/Lean/Linter/ConstructorAsVariable.lean
+++ b/src/Lean/Linter/ConstructorAsVariable.lean
@@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
     let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
-      tree.visitM' (preNode := fun ci info _ => do
+      tree.visitM' (postNode := fun ci info _ => do
         match info with
         | .ofTermInfo ti =>
           match ti.expr with
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 34c3e959e594..f7b19d16f20f 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -10,41 +10,55 @@ set_option linter.missingDocs true -- keep it documented
 
 /-! # Unused variable Linter
 
-This file implements the unused variable linter, which runs automatically on all commands
-and reports any local variables that are never referred to, using information from the info tree.
-
-It is not immediately obvious but this is a surprisingly expensive check without some optimizations.
-The main complication is that it can be difficult to determine what constitutes a "use".
-For example, we would like this to be considered a use of `x`:
+This file implements the unused variable linter, which runs automatically on all
+commands and reports any local variables that are never referred to, using
+information from the info tree.
+
+It is not immediately obvious but this is a surprisingly expensive check without
+some optimizations.  The main complication is that it can be difficult to
+determine what constitutes a "use" apart from direct references to a variable
+that we can easily find in the info tree.  For example, we would like this to be
+considered a use of `x`: 
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
 
-The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
-the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
-further into the tactic state we can see the `fvar` show up in the instantiation to the original
-goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
-instantiations to determine what happened after the fact, because tactics might skip the goal
-metavariable and instantiate some other metavariable created prior to it instead.
-
-Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
-metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
-linear in the size of the info tree, even though there are many metavariable contexts in all the
-intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
-so there is a lot of subterm sharing we can take advantage of.
+The final proof term is `fun x => x` so clearly `x` was used, but we can't make
+use of this because the final proof term is after we have abstracted over the
+original `fvar` for `x`. Instead, we make sure to store the proof term before
+abstraction but after instantiation of mvars in the info tree and retrieve it in
+the linter. Using the instantiated term is very important as redoing that step
+in the linter can be prohibitively expensive. The downside of special-casing the
+definition body in this way is that while it works for parameters, it does not
+work for local variables in the body, so we ignore them by default if any tactic
+infos are present (`linter.unusedVariables.analyzeTactics`).
+
+If we do turn on this option and look further into the tactic state, we can see
+the `fvar` show up in the instantiation to the original goal metavariable
+`?m : Nat := x`, but it is not always the case that we can follow metavariable
+instantiations to determine what happened after the fact, because tactics might
+skip the goal metavariable and instantiate some other metavariable created prior
+to it instead.  Instead, we use a (much more expensive) overapproximation, which
+is just to look through the entire metavariable context looking for occurrences
+of `x`. We use caching to ensure that this is still linear in the size of the
+info tree, even though there are many metavariable contexts in all the
+intermediate stages of elaboration; these are highly similar and make use of
+`PersistentHashMap` so there is a lot of subterm sharing we can take advantage
+of.
 
 ## The `@[unused_variables_ignore_fn]` attribute
 
-Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
-variables in these positions. For example:
+Some occurrences of variables are deliberately unused, or at least we don't want
+to lint on unused variables in these positions. For example:
 
 ```
 def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
                   -- ^ don't lint this unused variable because it is public API
 ```
 
-They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
-external syntax can also opt in to lint suppression, like so:
+They are generally a syntactic criterion, so we allow adding custom
+`IgnoreFunction`s so that external syntax can also opt in to lint suppression,
+like so:
 
 ```
 macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
@@ -77,6 +91,17 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
+/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
+register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
+  defValue := false
+  descr := "enable analysis of local variables in presence of tactic proofs\
+          \n\
+          \nBy default, the linter will limit itself to linting a declaration's parameters \
+            whenever tactic proofs are present as these can be expensive to analyze. Enabling this \
+            option extends linting to local variables both inside and outside tactic proofs, \
+            though it can also lead to some false negatives as intermediate tactic states may \
+            reference some variables without the declaration ultimately depending on them."
+}
 
 /-- Gets the status of `linter.unusedVariables` -/
 def getLinterUnusedVariables (o : Options) : Bool :=
@@ -356,55 +381,82 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
-    StateRefT References IO Unit := do
-  for tree in infoTrees do
-    tree.visitM' (preNode := fun ci info _ => do
-      match info with
-      | .ofTermInfo ti =>
-        match ti.expr with
-        | .const .. =>
-          if ti.isBinder then
-            let some range := info.range? | return
-            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-            modify fun s => { s with constDecls := s.constDecls.insert range }
-        | .fvar id .. =>
-          let some range := info.range? | return
-          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-          if ti.isBinder then
-            -- This is a local variable declaration.
-            let some ldecl := ti.lctx.find? id | return
-            -- Skip declarations which are outside the command syntax range, like `variable`s
-            -- (it would be confusing to lint these), or those which are macro-generated
-            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
-            let opts := ci.options
-            -- we have to check for the option again here because it can be set locally
-            if !getLinterUnusedVariables opts then return
-            let stx := skipDeclIdIfPresent info.stx
-            if let .str _ s := stx.getId then
-              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-              -- This is the suggested way to silence the warning
-              if s.startsWith "_" then return
-            -- Record this either as a new `fvarDefs`, or an alias of an existing one
-            modify fun s =>
-              if let some ref := s.fvarDefs[range]? then
-                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
-              else
-                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
-          else
-            -- Found a direct use, keep track of it
-            modify fun s => { s with fvarUses := s.fvarUses.insert id }
-        | _ => pure ()
-      | .ofTacticInfo ti =>
-        -- Keep track of the `MetavarContext` after a tactic for later
-        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
-      | .ofFVarAliasInfo i =>
-        -- record any aliases we find
-        modify fun s =>
-          let id := followAliases s.fvarAliases i.baseId
-          { s with fvarAliases := s.fvarAliases.insert i.id id }
-      | _ => pure ())
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
 where
+  go infoTrees ctx? := do
+    for tree in infoTrees do
+      tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
+        -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
+        let ignored ← read
+        match info with
+        | .ofTermInfo ti =>
+          -- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
+          -- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
+          -- parameters
+          if ti.elaborator == `MutualDef.body &&
+              !linter.unusedVariables.analyzeTactics.get ci.options then
+            -- the body is the only `Expr` we will analyze in this case
+            -- NOTE: we include it even if no tactics are present as at least for parameters we want
+            -- to lint only truly unused binders
+            let (e, _) := instantiateMVarsCore ci.mctx ti.expr
+            modify fun s => { s with
+              assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+            let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+            withReader (· || tacticsPresent) do
+              go children.toArray ci
+            return false
+          if ignored then return true
+          match ti.expr with
+          | .const .. =>
+            if ti.isBinder then
+              let some range := info.range? | return true
+              let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+              modify fun s => { s with constDecls := s.constDecls.insert range }
+          | .fvar id .. =>
+            let some range := info.range? | return true
+            let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+            if ti.isBinder then
+              -- This is a local variable declaration.
+              if ignored then return true
+              let some ldecl := ti.lctx.find? id | return true
+              -- Skip declarations which are outside the command syntax range, like `variable`s
+              -- (it would be confusing to lint these), or those which are macro-generated
+              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
+              let opts := ci.options
+              -- we have to check for the option again here because it can be set locally
+              if !getLinterUnusedVariables opts then return true
+              let stx := skipDeclIdIfPresent info.stx
+              if let .str _ s := stx.getId then
+                -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+                -- This is the suggested way to silence the warning
+                if s.startsWith "_" then return true
+              -- Record this either as a new `fvarDefs`, or an alias of an existing one
+              modify fun s =>
+                if let some ref := s.fvarDefs[range]? then
+                  { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+                else
+                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+            else
+              -- Found a direct use, keep track of it
+              modify fun s => { s with fvarUses := s.fvarUses.insert id }
+          | _ => pure ()
+          return true
+        | .ofTacticInfo ti =>
+          -- When ignoring new binders, no need to look at intermediate tactic states either as
+          -- references to binders outside the body will be covered by the body `Expr`
+          if ignored then return true
+          -- Keep track of the `MetavarContext` after a tactic for later
+          modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+          return true
+        | .ofFVarAliasInfo i =>
+          if ignored then return true
+          -- record any aliases we find
+          modify fun s =>
+            let id := followAliases s.fvarAliases i.baseId
+            { s with fvarAliases := s.fvarAliases.insert i.id id }
+          return true
+        | _ => return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
@@ -493,7 +545,7 @@ def unusedVariables : Linter where
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
         -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
+        fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 28b6b8a63611..34d202348d5e 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -40,27 +40,34 @@ structure InfoWithCtx where
   info : Elab.Info
   children : PersistentArray InfoTree
 
-/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
-and accumulating results on the way back up. -/
+/--
+Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
+accumulating results on the way back up. If `preNode` returns `false`, the children of the current
+node are skipped and `postNode` is invoked with an empty list of results.
+-/
 partial def InfoTree.visitM [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
-    : InfoTree → m (Option α) :=
-  go none
+    (ctx? : Option ContextInfo := none) : InfoTree → m (Option α) :=
+  go ctx?
 where go
   | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
   | some ctx, node i cs => do
-    preNode ctx i cs
-    let as ← cs.toList.mapM (go <| i.updateContext? ctx)
-    postNode ctx i cs as
+    let visitChildren ← preNode ctx i cs
+    if !visitChildren then
+      postNode ctx i cs []
+    else
+      let as ← cs.toList.mapM (go <| i.updateContext? ctx)
+      postNode ctx i cs as
   | none, node .. => panic! "unexpected context-free info tree node"
   | _, hole .. => pure none
 
 /-- `InfoTree.visitM` specialized to `Unit` return type -/
 def InfoTree.visitM' [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
-    (t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard
+    (ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
+  t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
 
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
@@ -410,6 +417,9 @@ where go ci?
     match ci?, i with
     | some ci, .ofTermInfo ti
     | some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
+      -- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
+      -- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
+      -- of making the `instantiateMVars` here a no-op and avoids further recursing into the body
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
       return expr.hasSorry
       -- we assume that `cs` are subterms of `ti.expr` and
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index aaf8ca4506de..0a9115549f05 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -31,49 +31,52 @@ a : α
       • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
       • match α, β, x, a with
         | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
-        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-          • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-        • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.636 -> _uniq.312
-        • FVarAlias α: _uniq.635 -> _uniq.310
-        • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-          • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.667 -> _uniq.312
-        • FVarAlias n: _uniq.666 -> _uniq.310
-        • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-          • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
+        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ MutualDef.body
+        • match α, β, x, a with
+          | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
+          | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+            • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+          • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • FVarAlias a: _uniq.636 -> _uniq.312
+          • FVarAlias α: _uniq.635 -> _uniq.310
+          • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+            • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+          • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • FVarAlias a: _uniq.667 -> _uniq.312
+          • FVarAlias n: _uniq.666 -> _uniq.310
+          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
+            • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
       • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
 [Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index 193e62afc09e..5f9cf56ae765 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -129,6 +129,7 @@ def nolintPatternVars (x : Option (Option Nat)) : Nat :=
   | some (some y) => (fun z => 1) 2
   | _ => 0
 
+set_option linter.unusedVariables.analyzeTactics true in
 set_option linter.unusedVariables.patternVars false in
 theorem nolintPatternVarsInduction (n : Nat) : True := by
   induction n with
@@ -188,9 +189,12 @@ opaque foo (x : Nat) : Nat
 opaque foo' (x : Nat) : Nat :=
   let y := 5
   3
+
+section
 variable (bar)
 variable (bar' : (x : Nat) → Nat)
 variable {α β} [inst : ToString α]
+end
 
 @[specialize]
 def specializeDef (x : Nat) : Nat := 3
@@ -210,6 +214,8 @@ opaque externConst (x : Nat) : Nat :=
   let y := 3
   5
 
+section
+variable {α : Type}
 
 macro "useArg " name:declId arg:ident : command => `(def $name ($arg : α) : α := $arg)
 useArg usedMacroVariable a
@@ -222,6 +228,7 @@ doNotUseArg unusedMacroVariable b
 def ignoreDoNotUse : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``doNotUse]
 
 doNotUseArg unusedMacroVariable2 b
+end
 
 macro "ignoreArg " id:declId sig:declSig : command => `(opaque $id $sig)
 ignoreArg ignoredMacroVariable (x : UInt32) : UInt32
@@ -246,6 +253,7 @@ def Nat.discriminate (n : Nat) (H1 : n = 0 → α) (H2 : ∀ m, n = succ m → 
   | 0 => H1 rfl
   | succ m => H2 m rfl
 
+/-! These are *not* linted against anymore as they are parameters used in the eventual body term. -/
 example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
@@ -267,3 +275,16 @@ inaccessible annotation.
 -/
 example : (x = y) → y = x
   | .refl _ => .refl _
+
+/-! We do lint parameters by default (`analyzeTactics false`) even when they have lexical uses -/
+
+theorem lexicalTacticUse (p : α → Prop) (ha : p a) (hb : p b) : p b := by
+  simp [ha, hb]
+
+/-!
+... however, `analyzeTactics true` consistently takes lexical uses for all variables into account
+-/
+
+set_option linter.unusedVariables.analyzeTactics true in
+theorem lexicalTacticUse' (p : α → Prop) (ha : p a) (hb : p b) : p b := by
+  simp [ha, hb]
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index 01bc4647cdf1..4842d0c98641 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -30,51 +30,37 @@ linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h`
+linterUnusedVariables.lean:138:9-138:10: warning: unused variable `h`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y`
+linterUnusedVariables.lean:152:8-152:9: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β`
+linterUnusedVariables.lean:155:20-155:21: warning: unused variable `β`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x`
+linterUnusedVariables.lean:156:7-156:8: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s`
+linterUnusedVariables.lean:166:6-166:7: warning: unused variable `s`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y`
+linterUnusedVariables.lean:190:6-190:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x`
+linterUnusedVariables.lean:200:19-200:20: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
+linterUnusedVariables.lean:204:6-204:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
+linterUnusedVariables.lean:209:6-209:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
+linterUnusedVariables.lean:214:6-214:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b`
+linterUnusedVariables.lean:225:32-225:33: warning: unused variable `b`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:236:27-236:28: error: don't know how to synthesize placeholder
+linterUnusedVariables.lean:243:27-243:28: error: don't know how to synthesize placeholder
 context:
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:237:0-237:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:238:0-238:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:239:29-241:7: error: unexpected token 'theorem'; expected '{' or tactic
-linterUnusedVariables.lean:239:27-239:29: error: unsolved goals
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
+linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:246:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
+linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h`
+linterUnusedVariables.lean:281:41-281:43: warning: unused variable `ha`
 note: this linter can be disabled with `set_option linter.unusedVariables false`