diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index b5297ee7ae..be8d65f609 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -63,7 +63,7 @@ noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabi
   ⟨choice h⟩
 
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
-  inhabited_of_nonempty (Exists.elim h (fun w hw => ⟨w⟩))
+  inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
 
 /- all propositions are Decidable -/
 noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
@@ -87,7 +87,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
     (fun (hp : ∃ x : α, p x) =>
       show {x : α // (∃ y : α, p y) → p x} from
       let xp := indefiniteDescription _ hp;
-      ⟨xp.val, fun h' => xp.property⟩)
+      ⟨xp.val, fun _ => xp.property⟩)
     (fun hp => ⟨choice h, fun h => absurd h hp⟩)
 
 /-- the Hilbert epsilon Function -/
diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean
index 0355e106ba..7c2a859d03 100644
--- a/src/Init/Control/ExceptCps.lean
+++ b/src/Init/Control/ExceptCps.lean
@@ -42,7 +42,7 @@ instance [Monad m] : MonadLift m (ExceptCpsT σ m) where
   monadLift := ExceptCpsT.lift
 
 instance [Inhabited ε] : Inhabited (ExceptCpsT ε m α) where
-  default := fun _ k₁ k₂ => k₂ default
+  default := fun _ _ k₂ => k₂ default
 
 @[simp] theorem run_pure [Monad m] : run (pure x : ExceptCpsT ε m α) = pure (Except.ok x) := rfl
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a9746d0347..91ed3a4d6e 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -407,6 +407,7 @@ variable {p q : Prop}
 theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
   byCases Or.inl Or.inr
 
+set_option linter.unusedVariables.funArgs false in
 theorem byContradiction [dec : Decidable p] (h : ¬p → False) : p :=
   byCases id (fun np => False.elim (h np))
 
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index f32c7367af..bd14f8aa9c 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -606,7 +606,7 @@ theorem extLit {n : Nat}
     (a b : Array α)
     (hsz₁ : a.size = n) (hsz₂ : b.size = n)
     (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ hi₂ => h i (hsz₁ ▸ hi₁)
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
 
 end Array
 
diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean
index 2f77822676..480d330924 100644
--- a/src/Init/Data/Format/Basic.lean
+++ b/src/Init/Data/Format/Basic.lean
@@ -214,8 +214,8 @@ private structure State where
 instance : MonadPrettyFormat (StateM State) where
   -- We avoid a structure instance update, and write these functions using pattern matching because of issue #316
   pushOutput s       := modify fun ⟨out, col⟩ => ⟨out ++ s, col + s.length⟩
-  pushNewline indent := modify fun ⟨out, col⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩
-  currColumn         := return (←get).column
+  pushNewline indent := modify fun ⟨out, _⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩
+  currColumn         := return (← get).column
   startTag _         := return ()
   endTags _          := return ()
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 8d695892f2..1873759a3a 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -399,8 +399,8 @@ instance [LT α] : LT (List α) := ⟨List.lt⟩
 
 instance hasDecidableLt [LT α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
   | [],    []    => isFalse (fun h => nomatch h)
-  | [],    _::bs => isTrue (List.lt.nil _ _)
-  | _::as, []    => isFalse (fun h => nomatch h)
+  | [],    _::_  => isTrue (List.lt.nil _ _)
+  | _::_, []     => isFalse (fun h => nomatch h)
   | a::as, b::bs =>
     match h a b with
     | isTrue h₁  => isTrue (List.lt.head _ _ h₁)
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index e634751af1..7a68b62a53 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -49,7 +49,7 @@ class Stream (stream : Type u) (value : outParam (Type v)) : Type (max u v) wher
   next? : stream → Option (value × stream)
 
 protected partial def Stream.forIn [Stream ρ α] [Monad m] (s : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
-  let inst : Inhabited (m β) := ⟨pure b⟩
+  let _ : Inhabited (m β) := ⟨pure b⟩
   let rec visit (s : ρ) (b : β) : m β := do
     match Stream.next? s with
     | some (a, s) => match (← f a b) with
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index 707337ed2d..935faaf1c8 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -52,7 +52,7 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   have := String.lt_next s pos
   apply Nat.sub.elim (motive := fun k => k < _) (utf8ByteSize s) (String.next s pos).1
-  . intro hle k he
+  . intro _ k he
     simp [he]; rw [Nat.add_comm, Nat.add_sub_assoc (Nat.le_of_lt this)]
     have := Nat.zero_lt_sub_of_lt this
     simp_all_arith
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 480bbad1ae..ebc3b487bd 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -300,8 +300,8 @@ def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
 
 def unsetTrailing (stx : Syntax) : Syntax :=
   match stx.getTailInfo with
-  | SourceInfo.original lead pos trail endPos => stx.setTailInfo (SourceInfo.original lead pos "".toSubstring endPos)
-  | _                                         => stx
+  | SourceInfo.original lead pos _ endPos => stx.setTailInfo (SourceInfo.original lead pos "".toSubstring endPos)
+  | _                                     => stx
 
 @[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
   if h : i < a.size then
@@ -337,8 +337,8 @@ partial def getHead? : Syntax → Option Syntax
   | stx@(atom info ..)  => info.getPos?.map fun _ => stx
   | stx@(ident info ..) => info.getPos?.map fun _ => stx
   | node SourceInfo.none _ args => args.findSome? getHead?
-  | stx@(node info _ _) => stx
-  | _                => none
+  | stx@(node ..) => stx
+  | _ => none
 
 def copyHeadTailInfoFrom (target source : Syntax) : Syntax :=
   target.setHeadInfo source.getHeadInfo |>.setTailInfo source.getTailInfo
@@ -921,6 +921,7 @@ instance (sep) : CoeTail (SepArray sep) (Array Syntax) where
 
 end Lean.Syntax.SepArray
 
+set_option linter.unusedVariables.funArgs false in
 /--
   Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
   the given tactic.
@@ -975,7 +976,6 @@ def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → S
   return result
 
 def expandInterpolatedStr (interpStr : Syntax) (type : Syntax) (toTypeFn : Syntax) : MacroM Syntax := do
-  let ref := interpStr
   let r ← expandInterpolatedStrChunks interpStr.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
   `(($r : $type))
 
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index df52a15d7b..bdbb78b0a3 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -229,7 +229,7 @@ inductive Loop where
   | mk
 
 @[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (loop : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop (b : β) : m β := do
     match ← f () b with
       | ForInStep.done b  => pure b
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 780ad4d325..c0f1466fee 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -288,7 +288,7 @@ theorem decide_eq_true : [s : Decidable p] → p → Eq (decide p) true
   | isTrue  _, _   => rfl
   | isFalse h₁, h₂ => absurd h₂ h₁
 
-theorem decide_eq_false : [s : Decidable p] → Not p → Eq (decide p) false
+theorem decide_eq_false : [Decidable p] → Not p → Eq (decide p) false
   | isTrue  h₁, h₂ => absurd h₁ h₂
   | isFalse _, _   => rfl
 
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 2f341a2ef2..747896b959 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -665,6 +665,7 @@ universe u
 
 namespace Lean
 
+set_option linter.unusedVariables.funArgs false in
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class Eval (α : Type u) where
   -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index da2b65cf2c..e9ba87bb90 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -55,7 +55,7 @@ namespace Prim
 
 /- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α` -/
 private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α :=
-  let inh : Inhabited α := Classical.inhabited_of_nonempty r.h
+  let _ : Inhabited α := Classical.inhabited_of_nonempty r.h
   pure default
 
 @[extern "lean_st_mk_ref"]
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 4ed5757294..fe825aa107 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -174,7 +174,7 @@ structure ParametricAttribute (α : Type) where
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   getParam : Name → Syntax → AttrM α
-  afterSet : Name → α → AttrM Unit := fun env _ _ => pure ()
+  afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
 
 def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index 34c1364c76..5c4834f56d 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -85,7 +85,7 @@ partial def visitFnBody (fnid : FunId) : FnBody → StateM ParamMap Unit
   | FnBody.case _ _ _ alts => alts.forM fun alt => visitFnBody fnid alt.body
   | e => do
     unless e.isTerminal do
-      let (instr, b) := e.split
+      let (_, b) := e.split
       visitFnBody fnid b
 
 def visitDecls (env : Environment) (decls : Array Decl) : StateM ParamMap Unit :=
@@ -176,7 +176,6 @@ def isOwned (x : VarId) : M Bool := do
 
 /- Updates `map[k]` using the current set of `owned` variables. -/
 def updateParamMap (k : ParamMap.Key) : M Unit := do
-  let currFn ← getCurrFn
   let s ← get
   match s.paramMap.find? k with
   | some ps => do
@@ -252,7 +251,7 @@ def collectExpr (z : VarId) : Expr → M Unit
     ownVar z *> ownArgsUsingParams xs ps
   | Expr.ap x ys        => ownVar z *> ownVar x *> ownArgs ys
   | Expr.pap _ xs       => ownVar z *> ownArgs xs
-  | other               => pure ()
+  | _                   => pure ()
 
 def preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit := do
   let ctx ← read
diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 45f8c92b8f..91dbf94989 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -61,7 +61,7 @@ def checkJP (j : JoinPointId) : M Unit := do
 def checkArg (a : Arg) : M Unit :=
   match a with
   | Arg.var x => checkVar x
-  | other     => pure ()
+  | _ => pure ()
 
 def checkArgs (as : Array Arg) : M Unit :=
   as.forM checkArg
@@ -147,14 +147,12 @@ def checkExpr (ty : IRType) : Expr → M Unit
 
 partial def checkFnBody : FnBody → M Unit
   | FnBody.vdecl x t v b    => do
-    checkExpr t v;
-    markVar x;
-    let ctx ← read
+    checkExpr t v
+    markVar x
     withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addLocal x t v }) (checkFnBody b)
   | FnBody.jdecl j ys v b => do
-    markJP j;
-    withParams ys (checkFnBody v);
-    let ctx ← read
+    markJP j
+    withParams ys (checkFnBody v)
     withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addJP j ys v }) (checkFnBody b)
   | FnBody.set x _ y b      => checkVar x *> checkArg y *> checkFnBody b
   | FnBody.uset x _ y b     => checkVar x *> checkVar y *> checkFnBody b
@@ -178,8 +176,8 @@ end Checker
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do
   let env ← getEnv
   match (Checker.checkDecl decl { env := env, decls := decls }).run' {} with
-  | Except.error msg => throw s!"IR check failed at '{decl.name}', error: {msg}"
-  | other            => pure ()
+  | .error msg => throw s!"IR check failed at '{decl.name}', error: {msg}"
+  | _ => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=
   decls.forM (checkDecl decls)
diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean
index 4371ca8351..0c0d39af90 100644
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -63,7 +63,7 @@ private def logMessageIfAux {α : Type} [ToFormat α] (optName : Name) (a : α)
 @[inline] def logMessageIf {α : Type} [ToFormat α] (cls : Name) (a : α) : CompilerM Unit :=
   logMessageIfAux (tracePrefixOptionName ++ cls) a
 
-@[inline] def logMessage {α : Type} [ToFormat α] (cls : Name) (a : α) : CompilerM Unit :=
+@[inline] def logMessage {α : Type} [ToFormat α] (a : α) : CompilerM Unit :=
   logMessageIfAux tracePrefixOptionName a
 
 @[inline] def modifyEnv (f : Environment → Environment) : CompilerM Unit :=
diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean
index faa7d0525e..dc6d02c127 100644
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -50,7 +50,7 @@ instance : BEq Value := ⟨Value.beq⟩
 
 partial def addChoice (merge : Value → Value → Value) : List Value → Value → List Value
   | [], v => [v]
-  | v₁@(ctor i₁ vs₁) :: cs, v₂@(ctor i₂ vs₂) =>
+  | v₁@(ctor i₁ _) :: cs, v₂@(ctor i₂ _) =>
     if i₁ == i₂ then merge v₁ v₂ :: cs
     else v₁ :: addChoice merge cs v₂
   | _, _ => panic! "invalid addChoice"
@@ -226,8 +226,6 @@ def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
 
 private partial def resetNestedJPParams : FnBody → M Unit
   | FnBody.jdecl _ ys _ k => do
-    let ctx ← read
-    let currFnIdx := ctx.currFnIdx
     ys.forM resetParamAssignment
     /- Remark we don't need to reset the parameters of joint-points
       nested in `b` since they will be reset if this JP is used. -/
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index ac91024003..3536eed947 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -118,7 +118,6 @@ def emitFnDecl (decl : Decl) (isExternal : Bool) : M Unit := do
   emitFnDeclAux decl cppBaseName isExternal
 
 def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := do
-  let cName := Name.mkSimple cNameStr
   let env ← getEnv
   let extC := isExternC env decl.name
   emitFnDeclAux decl cNameStr extC
@@ -641,7 +640,7 @@ end
 
 def emitDeclAux (d : Decl) : M Unit := do
   let env ← getEnv
-  let (vMap, jpMap) := mkVarJPMaps d
+  let (_, jpMap) := mkVarJPMaps d
   withReader (fun ctx => { ctx with jpMap := jpMap }) do
   unless hasInitAttr env d.name do
     match d with
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index a6d3816999..9b0b04c155 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -78,8 +78,8 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
           let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
           eraseProjIncForAux y bs mask keep
         else done ()
-      | other => done ()
-    | other => done ()
+      | _ => done ()
+    | _ => done ()
 
 /- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
@@ -235,7 +235,6 @@ def mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody := do
 -- Expand `bs; x := reset[n] y; b`
 partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
     (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody := do
-  let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b
   let (bs, mask) := eraseProjIncFor n y bs
   /- Remark: we may be duplicting variable/JP indices. That is, `bSlow` and `bFast` may
      have duplicate indices. We run `normalizeIds` to fix the ids after we have expand them. -/
diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index f06042663b..d63dfd1ad5 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -114,7 +114,7 @@ partial def formatFnBody (fnBody : FnBody) (indent : Nat := 2) : Format :=
     | FnBody.dec x n _ _ b       => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
     | FnBody.del x b             => "del " ++ format x ++ ";" ++ Format.line ++ loop b
     | FnBody.mdata d b           => "mdata " ++ format d ++ ";" ++ Format.line ++ loop b
-    | FnBody.case tid x xType cs => "case " ++ format x ++ " : " ++ format xType ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt loop indent c) Format.nil
+    | FnBody.case _ x xType cs   => "case " ++ format x ++ " : " ++ format xType ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt loop indent c) Format.nil
     | FnBody.jmp j ys            => "jmp " ++ format j ++ formatArray ys
     | FnBody.ret x               => "ret " ++ format x
     | FnBody.unreachable         => "⊥"
diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean
index 5e18318c5c..4b5c4a395a 100644
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -91,7 +91,7 @@ namespace FreeIndices
 abbrev Collector := IndexSet → IndexSet → IndexSet
 
 @[inline] private def skip : Collector :=
-  fun bv fv => fv
+  fun _ fv => fv
 
 @[inline] private def collectIndex (x : Index) : Collector :=
   fun bv fv => if bv.contains x then fv else fv.insert x
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index 52e032ab61..b71d961385 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -114,7 +114,7 @@ partial def normFnBody : FnBody → N FnBody
 
 def normDecl (d : Decl) : N Decl :=
   match d with
-  | Decl.fdecl (xs := xs) (body := b) .. => withParams xs fun xs => return d.updateBody! (← normFnBody b)
+  | Decl.fdecl (xs := xs) (body := b) .. => withParams xs fun _ => return d.updateBody! (← normFnBody b)
   | other => pure other
 
 end NormalizeIds
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index 1b274311ca..09d56f4079 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -262,7 +262,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
     let bLiveVars := collectLiveVars b ctx.jpLiveVarMap
     (b, bLiveVars)
   | FnBody.unreachable, _ => (FnBody.unreachable, {})
-  | other, ctx => (other, {}) -- unreachable if well-formed
+  | other, _ => (other, {}) -- unreachable if well-formed
 
 partial def visitDecl (env : Environment) (decls : Array Decl) (d : Decl) : Decl :=
   match d with
diff --git a/src/Lean/Compiler/IR/Sorry.lean b/src/Lean/Compiler/IR/Sorry.lean
index 028b8eeee0..4d1e05f6a1 100644
--- a/src/Lean/Compiler/IR/Sorry.lean
+++ b/src/Lean/Compiler/IR/Sorry.lean
@@ -40,7 +40,7 @@ partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
   | FnBody.case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
   | _ =>
     unless b.isTerminal do
-      let (instr, b) := b.split
+      let (_, b) := b.split
       visitFndBody b
 
 def visitDecl (d : Decl) : M Unit := do
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
index 1e70ca080a..792833d9b6 100644
--- a/src/Lean/Compiler/Specialize.lean
+++ b/src/Lean/Compiler/Specialize.lean
@@ -25,7 +25,7 @@ builtin_initialize specializeAttrs : EnumAttributes SpecializeAttributeKind ←
        In the new equation compiler we should pass all attributes and allow it to apply them to auxiliary definitions.
        In the current implementation, we workaround this issue by using functions such as `hasSpecializeAttrAux`.
      -/
-    (fun declName _ => pure ())
+    (fun _ _ => pure ())
     AttributeApplicationTime.beforeElaboration
 
 private partial def hasSpecializeAttrAux (env : Environment) (kind : SpecializeAttributeKind) (n : Name) : Bool :=
diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean
index 776d61f020..fd996d23e9 100644
--- a/src/Lean/Data/Trie.lean
+++ b/src/Lean/Data/Trie.lean
@@ -101,7 +101,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos
   loop t i (i, none)
 
 private partial def toStringAux {α : Type} : Trie α → List Format
-  | Trie.Node val map => map.fold (fun Fs c t =>
+  | Trie.Node _ map => map.fold (fun Fs c t =>
    format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
 
 instance {α : Type} : ToString (Trie α) :=
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 2fdb2e941f..8021663461 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -183,7 +183,7 @@ private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do
 
 /- Return true if the given type contains `OptParam` or `AutoParams` -/
 private def hasOptAutoParams (type : Expr) : M Bool := do
-  forallTelescopeReducing type fun xs type =>
+  forallTelescopeReducing type fun xs _ =>
     xs.anyM fun x => do
       let xType ← inferType x
       return xType.getOptParamDefault?.isSome || xType.getAutoParamTactic?.isSome
@@ -882,7 +882,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($(e).$field:ident) => elabFieldName e field
     | `($e |>.$field:ident) => elabFieldName e field
     | `($e[%$bracket $idx]) => elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `($id:ident@$_:term) =>
+    | `($_:ident@$_:term) =>
       throwError "unexpected occurrence of named pattern"
     | `($id:ident) => do
       elabAppFnId id [] lvals namedArgs args expectedType? explicit ellipsis overloaded acc
@@ -891,7 +891,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
     | `(@$id:ident) =>
       elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
-    | `(@$id:ident.{$us,*}) =>
+    | `(@$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
@@ -1022,11 +1022,11 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 `@e` for any term `e` also disables the insertion of implicit lambdas at this position. -/
 @[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$id:ident)         => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$id:ident.{$us,*}) => elabAtom stx expectedType?
-  | `(@($t))              => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                     => throwUnsupportedSyntax
+  | `(@$_:ident)         => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@($t))             => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
+  | `(@$t)               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                    => throwUnsupportedSyntax
 
 @[builtinTermElab choice] def elabChoice : TermElab := elabAtom
 @[builtinTermElab proj] def elabProj : TermElab := elabAtom
diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean
index 4ac980dfdc..eaeab846cb 100644
--- a/src/Lean/Elab/Arg.lean
+++ b/src/Lean/Elab/Arg.lean
@@ -30,6 +30,7 @@ def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : MetaM (Arra
     throwError "argument '{namedArg.name}' was already set"
   return namedArgs.push namedArg
 
+set_option linter.unusedVariables.funArgs false in
 partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array NamedArg × Array Arg × Bool) := do
   let (args, ellipsis) :=
     if args.isEmpty then
@@ -51,6 +52,7 @@ partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array N
       return (namedArgs, args.push $ Arg.stx stx)
   return (namedArgs, args, ellipsis)
 
+set_option linter.unusedVariables.funArgs false in
 def expandApp (stx : Syntax) (pattern := false) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
   let (namedArgs, args, ellipsis) ← expandArgs stx[1].getArgs
   return (stx[0], namedArgs, args, ellipsis)
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 8961155231..51da3249fa 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -57,8 +57,8 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
           let quotedArg ← quoteAutoTactic arg
           quotedArgs ← `(Array.push $quotedArgs $quotedArg)
       `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
-  | Syntax.atom info val => `(mkAtom $(quote val))
-  | Syntax.missing       => throwError "invalid auto tactic, tactic is missing"
+  | Syntax.atom _ val => `(mkAtom $(quote val))
+  | Syntax.missing    => throwError "invalid auto tactic, tactic is missing"
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
@@ -552,7 +552,7 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
 open Lean.Elab.Term.Quotation in
 @[builtinQuotPrecheck Lean.Parser.Term.fun] def precheckFun : Precheck
   | `(fun $binders* => $body) => do
-    let (binders, body, expandedPattern) ← liftMacroM <| expandFunBinders binders body
+    let (binders, body, _) ← liftMacroM <| expandFunBinders binders body
     let mut ids := #[]
     for b in binders do
       for v in ← matchBinder b do
@@ -567,7 +567,7 @@ open Lean.Elab.Term.Quotation in
     -- We can assume all `match` binders have been iteratively expanded by the above macro here, though
     -- we still need to call `expandFunBinders` once to obtain `binders` in a normal form
     -- expected by `elabFunBinder`.
-    let (binders, body, expandedPattern) ← liftMacroM <| expandFunBinders binders body
+    let (binders, body, _) ← liftMacroM <| expandFunBinders binders body
     elabFunBinders binders expectedType? fun xs expectedType? => do
       /- We ensure the expectedType here since it will force coercions to be applied if needed.
           If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
@@ -653,7 +653,6 @@ def expandLetEqnsDecl (letDecl : Syntax) : MacroM Syntax := do
   return mkNode `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
 
 def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
-  let ref     := stx
   let letDecl := stx[1][0]
   let body    := stx[3]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean
index eb022743f0..fe31dca209 100644
--- a/src/Lean/Elab/BindersUtil.lean
+++ b/src/Lean/Elab/BindersUtil.lean
@@ -32,7 +32,6 @@ def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat :=
 -/
 def expandMatchAlt (matchAlt : Syntax) : Array Syntax :=
   let patss := matchAlt[1]
-  let rhs   := matchAlt[3]
   if patss.getArgs.size ≤ 1 then
     #[matchAlt]
   else
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 71a6b1726b..e7b73520be 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -103,7 +103,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
     let cmd := cmds.get ⟨i, h⟩;
     catchInternalId unsupportedSyntaxExceptionId
       (elabCommand cmd)
-      (fun ex => elabChoiceAux cmds (i+1))
+      (fun _ => elabChoiceAux cmds (i+1))
   else
     throwUnsupportedSyntax
 
@@ -113,7 +113,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
 @[builtinCommandElab «universe»] def elabUniverse : CommandElab := fun n => do
   n[1].forArgsM addUnivLevel
 
-@[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab := fun stx => do
+@[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
   match (← getEnv).addDecl Declaration.quotDecl with
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
@@ -124,7 +124,6 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   let ns ← resolveNamespace id
   let currNamespace ← getCurrNamespace
   if ns == currNamespace then throwError "invalid 'export', self export"
-  let env ← getEnv
   let ids := stx[3].getArgs
   let aliases ← ids.foldlM (init := []) fun (aliases : List (Name × Name)) (idStx : Syntax) => do
     let id := idStx.getId
@@ -307,7 +306,6 @@ private def mkRunEval (e : Expr) : MetaM Expr := do
 unsafe def elabEvalUnsafe : CommandElab
   | `(#eval%$tk $term) => do
     let n := `_eval
-    let ctx ← read
     let addAndCompile (value : Expr) : TermElabM Unit := do
       let (value, _) ← Term.levelMVarToParam (← instantiateMVars value)
       let type ← inferType value
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index a67317e434..0583d4f4e6 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -41,7 +41,7 @@ are turned into a new anonymous constructor application. For example,
       let expectedType ← whnf expectedType
       matchConstInduct expectedType.getAppFn
         (fun _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type {indentExpr expectedType}")
-        (fun ival us => do
+        (fun ival _ => do
           match ival.ctors with
           | [ctor] =>
             let cinfo ← getConstInfoCtor ctor
@@ -141,7 +141,7 @@ then aborted. -/
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
 
 /-- A shorthand for `panic! "unreachable code has been reached"`. -/
-@[builtinMacro Lean.Parser.Term.unreachable]  def expandUnreachable : Macro := fun stx =>
+@[builtinMacro Lean.Parser.Term.unreachable]  def expandUnreachable : Macro := fun _ =>
   `(panic! "unreachable code has been reached")
 
 /-- `assert! cond` panics if `cond` evaluates to `false`. -/
@@ -269,7 +269,7 @@ where
     else
       throw <| Macro.Exception.error stx "unexpected parentheses notation"
 
-@[builtinTermElab paren] def elabParen : TermElab := fun stx expectedType? => do
+@[builtinTermElab paren] def elabParen : TermElab := fun stx _ => do
   match stx with
   | `(($e : $type)) =>
     let type ← withSynthesize (mayPostpone := true) <| elabType type
@@ -362,7 +362,6 @@ See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lea
          let h ← elabTerm hStx none
          let hType ← inferType h
          let hTypeAbst ← kabstract hType lhs
-         let hTypeNew := hTypeAbst.instantiate1 rhs
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 57464f43e0..70afe85867 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -146,7 +146,6 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
   let mvarId := mvar.mvarId!
   let ref ← getRef
-  let declName? ← getDeclName?
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
@@ -159,7 +158,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtinTermElab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtinTermElab cdot] def elabBadCDot : TermElab := fun stx _ =>
+@[builtinTermElab cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtinTermElab str] def elabStrLit : TermElab := fun stx _ => do
@@ -185,7 +184,7 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
   registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
   return r
 
-@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab :=  fun stx expectedType? => do
+@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab :=  fun stx _ => do
   match stx[1].isNatLit? with
   | some val => return mkRawNatLit val
   | none     => throwIllFormedSyntax
@@ -250,7 +249,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   else
     return e
 
-@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab := fun stx expectedType? =>
+@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab := fun stx _ =>
   match stx[2].isStrLit? with
   | none     => throwIllFormedSyntax
   | some msg => do
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 59b1a1e973..3cc6e8be99 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -343,10 +343,10 @@ private def mkMetaContext : Meta.Context := {
 }
 
 def getBracketedBinderIds : Syntax → Array Name
-  | `(bracketedBinder|($ids* $[: $ty?]? $(annot?)?)) => ids.map Syntax.getId
+  | `(bracketedBinder|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId
   | `(bracketedBinder|{$ids* $[: $ty?]?})            => ids.map Syntax.getId
-  | `(bracketedBinder|[$id : $ty])                   => #[id.getId]
-  | `(bracketedBinder|[$ty])                         => #[Name.anonymous]
+  | `(bracketedBinder|[$id : $_])                    => #[id.getId]
+  | `(bracketedBinder|[$_])                          => #[Name.anonymous]
   | _                                                => #[]
 
 private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := Id.run do
@@ -377,7 +377,7 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
   let x : MetaM _      := (observing x).run (mkTermContext ctx s declName?) (mkTermState scope s)
   let x : CoreM _      := x.run mkMetaContext {}
   let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope }
-  let (((ea, termS), metaS), coreS) ← liftEIO x
+  let (((ea, termS), _), coreS) ← liftEIO x
   modify fun s => { s with
     env             := coreS.env
     nextMacroScope  := coreS.nextMacroScope
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 62d4f1f4d0..8639f0a2df 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -25,7 +25,7 @@ private def ensureValidNamespace (name : Name) : MacroM Unit := do
 
 /- Auxiliary function for `expandDeclNamespace?` -/
 private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × Syntax)) := do
-  let (id, optUnivDeclStx) := expandDeclIdCore declId
+  let (id, _) := expandDeclIdCore declId
   let scpView := extractMacroScopes id
   match scpView.name with
   | Name.str Name.anonymous _ _ => return none
@@ -73,7 +73,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let declId             := stx[1]
   let (binders, typeStx) := expandDeclSig stx[2]
   let scopeLevelNames ← getLevelNames
-  let ⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
+  let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
   addDeclarationRanges declName stx
   runTermElabM declName fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders binders.getArgs fun xs => do
     Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index e3d7ae9fd3..04e4f3ae87 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -100,7 +100,7 @@ def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name
       ref.get
     set savedState
     liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ result)
-  catch ex =>
+  catch _ =>
     set savedState
     mkFreshInstanceName
 
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index fac0075094..56c02dd72c 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -11,10 +11,10 @@ namespace Lean.Elab.Deriving.BEq
 open Lean.Parser.Term
 open Meta
 
-def mkBEqHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
-  mkHeader ctx `BEq 2 indVal
+def mkBEqHeader (indVal : InductiveVal) : TermElabM Header := do
+  mkHeader `BEq 2 indVal
 
-def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
+def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -71,8 +71,8 @@ where
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[i]
   let indVal     := ctx.typeInfos[i]
-  let header     ← mkBEqHeader ctx indVal
-  let mut body   ← mkMatch ctx header indVal auxFunName
+  let header     ← mkBEqHeader indVal
+  let mut body   ← mkMatch header indVal auxFunName
   if ctx.usePartial then
     let letDecls ← mkLocalInstanceLetDecls ctx `BEq header.argNames
     body ← mkLet letDecls body
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index d10fed3f2c..188c9af683 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -12,10 +12,10 @@ namespace Lean.Elab.Deriving.DecEq
 open Lean.Parser.Term
 open Meta
 
-def mkDecEqHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
-  mkHeader ctx `DecidableEq 2 indVal
+def mkDecEqHeader (indVal : InductiveVal) : TermElabM Header := do
+  mkHeader `DecidableEq 2 indVal
 
-def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
+def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -86,8 +86,8 @@ where
 def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]
   let indVal     :=ctx.typeInfos[0]
-  let header     ← mkDecEqHeader ctx indVal
-  let mut body   ← mkMatch ctx header indVal auxFunName header.argNames
+  let header     ← mkDecEqHeader indVal
+  let mut body   ← mkMatch header indVal auxFunName
   let binders    := header.binders
   let type       ← `(Decidable ($(mkIdent header.targetNames[0]) = $(mkIdent header.targetNames[1])))
   `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : $type:term := $body:term)
@@ -163,7 +163,6 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
   liftTermElabM none <| mkEnumOfNatThm declName
   let ofNatIdent  := mkIdent (Name.mkStr declName "ofNat")
   let auxThmIdent := mkIdent (Name.mkStr declName "ofNat_toCtorIdx")
-  let indVal ← getConstInfoInduct declName
   let cmd ← `(
     instance : DecidableEq $(mkIdent declName) :=
       fun x y =>
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 00640796b0..3e91cb78ab 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -24,7 +24,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
     if isStructure (← getEnv) declNames[0] then
       let cmds ← liftTermElabM none <| do
         let ctx ← mkContext "toJson" declNames[0]
-        let header ← mkHeader ctx ``ToJson 1 ctx.typeInfos[0]
+        let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]
         let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
         let fields : Array Syntax ← fields.mapM fun field => do
           let (isOptField, nm) := mkJsonField field
@@ -45,7 +45,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let mkToJson (id : Syntax) (type : Expr) : TermElabM Syntax := do
           if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident)
           else ``(toJson $id:ident)
-        let header ← mkHeader ctx ``ToJson 1 ctx.typeInfos[0]
+        let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]
         let discrs ← mkDiscrs header indVal
         let alts ← mkAlts indVal fun ctor args userNames => do
           match args, userNames with
@@ -76,7 +76,7 @@ where
     (rhs : ConstructorVal → Array (Syntax × Expr) → (Option $ Array Name) → TermElabM Syntax) : TermElabM (Array Syntax) := do
   indVal.ctors.toArray.mapM fun ctor => do
     let ctorInfo ← getConstInfoCtor ctor
-    forallTelescopeReducing ctorInfo.type fun xs type => do
+    forallTelescopeReducing ctorInfo.type fun xs _ => do
       let mut patterns := #[]
       -- add `_` pattern for indices
       for _ in [:indVal.numIndices] do
@@ -105,7 +105,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
     if isStructure (← getEnv) declNames[0] then
       let cmds ← liftTermElabM none <| do
         let ctx ← mkContext "fromJson" declNames[0]
-        let header ← mkHeader ctx ``FromJson 0 ctx.typeInfos[0]
+        let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]
         let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
         let jsonFields := fields.map (Prod.snd ∘ mkJsonField)
         let fields := fields.map mkIdent
@@ -120,9 +120,8 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
       let indVal ← getConstInfoInduct declNames[0]
       let cmds ← liftTermElabM none <| do
         let ctx ← mkContext "fromJson" declNames[0]
-        let header ← mkHeader ctx ``FromJson 0 ctx.typeInfos[0]
+        let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]
         let fromJsonFuncId := mkIdent ctx.auxFunNames[0]
-        let discrs ← mkDiscrs header indVal
         let alts ← mkAlts indVal fromJsonFuncId
         let mut auxCmd ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
         if ctx.usePartial then
@@ -150,7 +149,7 @@ where
   let alts ←
     indVal.ctors.toArray.mapM fun ctor => do
       let ctorInfo ← getConstInfoCtor ctor
-      forallTelescopeReducing ctorInfo.type fun xs type => do
+      forallTelescopeReducing ctorInfo.type fun xs _ => do
         let mut binders := #[]
         let mut userNames := #[]
         for i in [:ctorInfo.numFields] do
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index 4eb37b8710..0c036e8684 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -12,10 +12,10 @@ open Command
 open Lean.Parser.Term
 open Meta
 
-def mkHashableHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
-  mkHeader ctx `Hashable 1 indVal
+def mkHashableHeader (indVal : InductiveVal) : TermElabM Header := do
+  mkHeader `Hashable 1 indVal
 
-def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFuncIdx : Nat) : TermElabM Syntax := do
+def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -27,8 +27,7 @@ where
     let allIndVals := indVal.all.toArray
     for ctorName in indVal.ctors do
       let ctorInfo ← getConstInfoCtor ctorName
-      let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
-        let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
         let mut patterns := #[]
         -- add `_` pattern for indices
         for _ in [:indVal.numIndices] do
@@ -58,8 +57,8 @@ where
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[i]
   let indVal     := ctx.typeInfos[i]
-  let header     ← mkHashableHeader ctx indVal
-  let body       ← mkMatch ctx header indVal i
+  let header     ← mkHashableHeader indVal
+  let body       ← mkMatch ctx header indVal
   let binders    := header.binders
   if ctx.usePartial then
     -- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index 548bafff11..0e398468d9 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -11,10 +11,10 @@ namespace Lean.Elab.Deriving.Ord
 open Lean.Parser.Term
 open Meta
 
-def mkOrdHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
-  mkHeader ctx `Ord 2 indVal
+def mkOrdHeader (indVal : InductiveVal) : TermElabM Header := do
+  mkHeader `Ord 2 indVal
 
-def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
+def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -67,8 +67,8 @@ where
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[i]
   let indVal     := ctx.typeInfos[i]
-  let header     ← mkOrdHeader ctx indVal
-  let mut body   ← mkMatch ctx header indVal auxFunName
+  let header     ← mkOrdHeader indVal
+  let mut body   ← mkMatch header indVal
   if ctx.usePartial || indVal.isRec then
     let letDecls ← mkLocalInstanceLetDecls ctx `Ord header.argNames
     body ← mkLet letDecls body
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 835b1719a9..f57ad1ea30 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -13,14 +13,13 @@ open Lean.Parser.Term
 open Meta
 open Std
 
-def mkReprHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
-  let prec ← `(prec)
-  let header ← mkHeader ctx `Repr 1 indVal
+def mkReprHeader (indVal : InductiveVal) : TermElabM Header := do
+  let header ← mkHeader `Repr 1 indVal
   return { header with
     binders := header.binders.push (← `(explicitBinderF| (prec : Nat)))
   }
 
-def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
+def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
   let ctorVal ← getConstInfoCtor indVal.ctors.head!
   let fieldNames := getStructureFields (← getEnv) indVal.name
   let numParams  := indVal.numParams
@@ -44,7 +43,7 @@ def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) :
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ repr ($target.$(mkIdent fieldName):ident))
     `(Format.bracket "{ " $fields:term " }")
 
-def mkBodyForInduct (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
+def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -53,7 +52,7 @@ where
     let mut alts := #[]
     for ctorName in indVal.ctors do
       let ctorInfo ← getConstInfoCtor ctorName
-      let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
         let mut patterns := #[]
         -- add `_` pattern for indices
         for _ in [:indVal.numIndices] do
@@ -79,17 +78,17 @@ where
       alts := alts.push alt
     return alts
 
-def mkBody (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
+def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
   if isStructure (← getEnv) indVal.name then
-    mkBodyForStruct ctx header indVal
+    mkBodyForStruct header indVal
   else
-    mkBodyForInduct ctx header indVal auxFunName
+    mkBodyForInduct header indVal auxFunName
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[i]
   let indVal     := ctx.typeInfos[i]
-  let header     ← mkReprHeader ctx indVal
-  let mut body   ← mkBody ctx header indVal auxFunName
+  let header     ← mkReprHeader indVal
+  let mut body   ← mkBody header indVal auxFunName
   if ctx.usePartial then
     let letDecls ← mkLocalInstanceLetDecls ctx `Repr header.argNames
     body ← mkLet letDecls body
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index d81e57f9f6..d37d312e8d 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -129,7 +129,7 @@ structure Header where
   targetNames : Array Name
   targetType  : Syntax
 
-def mkHeader (ctx : Context) (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElabM Header := do
+def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElabM Header := do
   let argNames      ← mkInductArgNames indVal
   let binders       ← mkImplicitBinders argNames
   let targetType    ← mkInductiveApp indVal argNames
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index c8f1632d63..9687028dc8 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -362,7 +362,7 @@ partial def pullExitPointsAux : VarSet → Code → StateRefT (Array JPDecl) Ter
   | rs, Code.seq e k                 => return Code.seq e (← pullExitPointsAux rs k)
   | rs, Code.ite ref x? o c t e      => return Code.ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
   | rs, Code.«match» ref g ds t alts => return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
-  | rs, c@(Code.jmp _ _ _)           => return  c
+  | _,  c@(Code.jmp _ _ _)           => return  c
   | rs, Code.«break» ref             => mkSimpleJmp ref rs (Code.«break» ref)
   | rs, Code.«continue» ref          => mkSimpleJmp ref rs (Code.«continue» ref)
   | rs, Code.«return» ref val        => mkJmp ref rs val (fun y => return Code.«return» ref y)
@@ -940,7 +940,6 @@ def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFr
     return mkNode ``Lean.Parser.Term.letrec #[letRecToken, letRecDecls, mkNullNode, k]
   else if kind == ``Lean.Parser.Term.doLetArrow then
     let arg := decl[2]
-    let ref := arg
     if arg.getKind == ``Lean.Parser.Term.doIdDecl then
       let id     := arg[0]
       let type   := expandOptType id arg[1]
@@ -1266,7 +1265,6 @@ mutual
      ```
   -/
   partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    let ref     := doLetArrow
     let decl    := doLetArrow[2]
     if decl.getKind == ``Lean.Parser.Term.doIdDecl then
       let y := decl[0]
@@ -1318,7 +1316,6 @@ mutual
      ```
   -/
   partial def doReassignArrowToCode (doReassignArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    let ref  := doReassignArrow
     let decl := doReassignArrow[0]
     if decl.getKind == ``Lean.Parser.Term.doIdDecl then
       let doElem := decl[3]
@@ -1357,7 +1354,6 @@ mutual
      "unless " >> termParser >> "do " >> doSeq
      ```  -/
   partial def doUnlessToCode (doUnless : Syntax) (doElems : List Syntax) : M CodeBlock := withRef doUnless do
-    let ref   := doUnless
     let cond  := doUnless[1]
     let doSeq := doUnless[3]
     let body ← doSeqToCode (getDoSeqElems doSeq)
@@ -1481,7 +1477,6 @@ mutual
     ```
   -/
   partial def doTryToCode (doTry : Syntax) (doElems: List Syntax) : M CodeBlock := do
-    let ref := doTry
     let tryCode ← doSeqToCode (getDoSeqElems doTry[1])
     let optFinally := doTry[3]
     let catches ← doTry[2].getArgs.mapM fun catchStx => do
@@ -1547,7 +1542,6 @@ mutual
           doSeqToCode (liftedDoElems ++ [doElem] ++ doElems)
         else
           let ref := doElem
-          let concatWithRest (c : CodeBlock) : M CodeBlock := concatWith c doElems
           let k := doElem.getKind
           if k == ``Lean.Parser.Term.doLet then
             let vars ← getDoLetVars doElem
diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index 0c2c3ea6d6..af767ea8e1 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -82,7 +82,6 @@ def expandElab : Macro
     elab$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* :
       $cat $[<= $expectedType?]? => $rhs) => do
     let prio    ← evalOptPrio prio?
-    let catName := cat.getId
     let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
     -- name
     let name ← match name? with
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index ea64f6499c..10ddb85a2a 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -36,11 +36,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
         let forInInstance ←
           try
             mkAppM ``ForIn #[m, colType, elemType]
-          catch
-            ex => tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+          catch _ =>
+            tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
         | LOption.some _   =>
-          let ref ← getRef
           let forInFn ← mkConst ``forIn
           elabAppArgs forInFn #[] #[Arg.stx col, Arg.stx init, Arg.stx body] expectedType? (explicit := false) (ellipsis := false)
         | LOption.undef    => tryPostpone; throwForInFailure forInInstance
@@ -61,11 +60,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           try
             let memType ← mkFreshExprMVar (← mkAppM ``Membership #[elemType, colType])
             mkAppM ``ForIn' #[m, colType, elemType, memType]
-          catch
-            ex => tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+          catch _ =>
+            tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
         | LOption.some _   =>
-          let ref ← getRef
           let forInFn ← mkConst ``forIn'
           elabAppArgs forInFn #[] #[Arg.expr colFVar, Arg.stx init, Arg.stx body] expectedType? (explicit := false) (ellipsis := false)
         | LOption.undef    => tryPostpone; throwForInFailure forInInstance
@@ -327,7 +325,6 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       let lhs ← toBoolIfNecessary lhs
       let rhs ← toBoolIfNecessary rhs
       let lhsType ← inferType lhs
-      let rhsType ← inferType rhs
       let rhs ← ensureHasType lhsType rhs
       elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false)
     else
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 0bf40d4702..631e5a8e82 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -57,7 +57,6 @@ def processCommand : FrontendM Bool := do
   let pstate ← getParserState
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
-  let pos := ictx.fileMap.toPosition pstate.pos
   match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
   | (cmd, ps, messages) =>
     modify fun s => { s with commands := s.commands.push cmd }
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index 18cab54e25..505b50f375 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -33,7 +33,7 @@ def parseImports (input : String) (fileName : Option String := none) : IO (List
 
 @[export lean_print_imports]
 def printImports (input : String) (fileName : Option String) : IO Unit := do
-  let (deps, pos, log) ← parseImports input fileName
+  let (deps, _, _) ← parseImports input fileName
   for dep in deps do
     let fname ← findOLean dep.module
     IO.println fname
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 33ea7bf85e..8f3cfe7cea 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -448,7 +448,7 @@ def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLC
 @[inline] def withInfoHole [MonadFinally m] [Monad m] [MonadInfoTree m] (mvarId : MVarId) (x : m α) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
-    Prod.fst <$> MonadFinally.tryFinally' x fun a? => modifyInfoState fun s =>
+    Prod.fst <$> MonadFinally.tryFinally' x fun _ => modifyInfoState fun s =>
       if s.trees.size > 0 then
         { s with trees := treesSaved, assignment := s.assignment.insert mvarId s.trees[s.trees.size - 1] }
       else
diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean
index 38f38bf5ec..2935e9e274 100644
--- a/src/Lean/Elab/MacroArgUtil.lean
+++ b/src/Lean/Elab/MacroArgUtil.lean
@@ -19,12 +19,12 @@ def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do
   let pat ← match stx with
     | `(stx| $s:str)      => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
     | `(stx| &$s:str)     => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
-    | `(stx| optional($stx)) => pure <| mkSplicePat `optional id "?"
-    | `(stx| many($stx))     => pure <| mkSplicePat `many id "*"
-    | `(stx| many1($stx))    => pure <| mkSplicePat `many id "*"
-    | `(stx| sepBy($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
+    | `(stx| optional($_)) => pure <| mkSplicePat `optional id "?"
+    | `(stx| many($_))     => pure <| mkSplicePat `many id "*"
+    | `(stx| many1($_))    => pure <| mkSplicePat `many id "*"
+    | `(stx| sepBy($_, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
       pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
-    | `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
+    | `(stx| sepBy1($_, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
       pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
     | _ => match id? with
       -- if there is a binding, we assume the user knows what they are doing
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 3ae271a107..176e73dc85 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -83,18 +83,17 @@ structure ElabMatchTypeAndDiscrsResult where
 
 private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptMotive : Syntax) (matchAltViews : Array MatchAltView) (expectedType : Expr)
       : TermElabM ElabMatchTypeAndDiscrsResult := do
-  let numDiscrs := discrStxs.size
   if matchOptMotive.isNone then
     elabDiscrs 0 #[]
   else
     -- motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> termParser >> ")"
     let matchTypeStx := matchOptMotive[0][3]
     let matchType ← elabType matchTypeStx
-    let (discrs, isDep) ← elabDiscrsWitMatchType matchType expectedType
+    let (discrs, isDep) ← elabDiscrsWitMatchType matchType
     return { discrs := discrs, matchType := matchType, isDep := isDep, alts := matchAltViews }
 where
   /- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user.  -/
-  elabDiscrsWitMatchType (matchType : Expr) (expectedType : Expr) : TermElabM (Array Discr × Bool) := do
+  elabDiscrsWitMatchType (matchType : Expr) : TermElabM (Array Discr × Bool) := do
     let mut discrs := #[]
     let mut i := 0
     let mut matchType := matchType
@@ -150,13 +149,13 @@ def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array Matc
     pure { matchAlt with patterns := patterns }
 
 private def getMatchGeneralizing? : Syntax → Option Bool
-  | `(match (generalizing := true)  $[$motive]? $discrs,* with $alts:matchAlt*) => some true
-  | `(match (generalizing := false) $[$motive]? $discrs,* with $alts:matchAlt*) => some false
+  | `(match (generalizing := true)  $[$motive]? $_discrs,* with $_alts:matchAlt*) => some true
+  | `(match (generalizing := false) $[$motive]? $_discrs,* with $_alts:matchAlt*) => some false
   | _ => none
 
 /- Given `stx` a match-expression, return its alternatives. -/
 private def getMatchAlts : Syntax → Array MatchAltView
-  | `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) =>
+  | `(match $[$gen]? $[$motive]? $_discrs,* with $alts:matchAlt*) =>
     alts.filterMap fun alt => match alt with
       | `(matchAltExpr| | $patterns,* => $rhs) => some {
           ref      := alt,
@@ -427,7 +426,7 @@ where
    let map : ST.Ref σ (ExprMap Expr) ← ST.mkRef {}
    e.forEach fun e => do
      match patternWithRef? e with
-     | some (ref, b) => map.modify (·.insert b e)
+     | some (_, b) => map.modify (·.insert b e)
      | none => return ()
    map.get
 
@@ -511,7 +510,7 @@ partial def normalize (e : Expr) : M Expr := do
         else
           matchConstCtor e.getAppFn
             (fun _ => return mkInaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e)))
-            (fun v us => do
+            (fun v _ => do
               let args := e.getAppArgs
               unless args.size == v.numParams + v.numFields do
                 throwInvalidPattern e
@@ -652,8 +651,8 @@ where
   /- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/
   go (p : Expr) : ReaderT Bool TermElabM Expr := do
     match p with
-    | .forallE n d b bi => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
-    | .lam n d b bi     => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
+    | .forallE n d b _  => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
+    | .lam n d b _      => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
     | .letE n t v b ..  => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
     | .app f a _        => return mkApp (← go f) (← go a)
     | .proj _ _ b _     => return p.updateProj! (← go b)
@@ -924,7 +923,7 @@ where
       let matchType ←
         try
           updateMatchType indices matchType
-        catch ex =>
+        catch _ =>
           throwEx first
       let ref ← getRef
       trace[Elab.match] "new indices to add as discriminants: {indices}"
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 8d3b27b839..c55214e1b8 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -164,7 +164,7 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
 private def expandWhereStructInst : Macro
   | `(Parser.Command.whereStructInst|where $[$decls:letDecl$[;]?]*) => do
     let letIdDecls ← decls.mapM fun stx => match stx with
-      | `(letDecl|$decl:letPatDecl)  => Macro.throwErrorAt stx "patterns are not allowed here"
+      | `(letDecl|$_decl:letPatDecl)  => Macro.throwErrorAt stx "patterns are not allowed here"
       | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl
       | `(letDecl|$decl:letIdDecl)   => pure decl
       | _                               => Macro.throwUnsupported
@@ -708,7 +708,7 @@ def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool :=
     }
     addInstance instName AttributeKind.global (eval_prio default)
     return true
-  catch ex =>
+  catch _ =>
     return false
 
 /-- Remove auxiliary match discriminant let-declarations. -/
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 86eb15972b..5260ff91c2 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -46,7 +46,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
 /-- Try to derive a `SimpleDelab` from a notation.
     The notation must be of the form `notation ... => c var_1 ... var_n`
     where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/
-def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do
+def mkSimpleDelab (attrKind : Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do
   match qrhs with
   | `($c:ident $args*) =>
     let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
@@ -95,7 +95,7 @@ private def expandNotationAux (ref : Syntax)
   if isLocalAttrKind attrKind then
     -- Make sure the quotation pre-checker takes section variables into account for local notation.
     macroDecl ← `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
-  match (← mkSimpleDelab attrKind vars pat qrhs |>.run) with
+  match (← mkSimpleDelab attrKind pat qrhs |>.run) with
   | some delabDecl => return mkNullNode #[stxDecl, macroDecl, delabDecl]
   | none           => return mkNullNode #[stxDecl, macroDecl]
 
diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean
index 62a2bf21ef..5dff71bfb9 100644
--- a/src/Lean/Elab/Open.lean
+++ b/src/Lean/Elab/Open.lean
@@ -57,7 +57,7 @@ private def elabOpenHiding (n : Syntax) : M (m:=m) Unit := do
   let ns ← resolveNamespace n[0].getId
   let mut ids : List Name := []
   for idStx in n[2].getArgs do
-    let declName ← resolveId ns idStx
+    let _ ← resolveId ns idStx
     let id := idStx.getId
     ids := id::ids
   addOpenDecl (OpenDecl.simple ns ids)
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 14cfae6797..57474f573a 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -31,7 +31,7 @@ def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
 
 def funext? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) := target.eq? | return none
+  let some (_, _, rhs) := target.eq? | return none
   unless rhs.isLambda do return none
   commitWhenSome? do
     let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | return none
diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
index 3c2f372b9e..fa99a471fc 100644
--- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean
+++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
@@ -13,7 +13,7 @@ private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option E
       return some (← mkOfNonempty type)
     else
       return some (← mkDefault type)
-  catch ex =>
+  catch _ =>
     return none
 
 private def findAssumption? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) := do
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index e28ff09163..3cd6335f1d 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -90,7 +90,7 @@ private partial def toBelow (below : Expr) (numIndParams : Nat) (recArg : Expr)
 def refinedArgType (matcherApp : MatcherApp) (arg : Expr) : MetaM Bool := do
   let argType ← inferType arg
   (Array.zip matcherApp.alts matcherApp.altNumParams).anyM fun (alt, numParams) =>
-    lambdaTelescope alt fun xs altBody => do
+    lambdaTelescope alt fun xs _ => do
       if xs.size >= numParams then
         let refinedArg := xs[numParams - 1]
         return !(← isDefEq (← inferType refinedArg) argType)
@@ -114,7 +114,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
       withLetDecl n (← loop below type) (← loop below val) fun x => do
         mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
     | Expr.mdata d b _   =>
-      if let some stx := getRecAppSyntax? e then
+      if let some _ := getRecAppSyntax? e then
         loop below b
       else
         return mkMData d (← loop below b)
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
index 9f83cd62c9..7c1db7ba23 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
@@ -90,7 +90,6 @@ def mkIndPredBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
     let FType ← instantiateForall FType recArgInfo.indIndices
     instantiateForall FType #[major]
   forallBoundedTelescope FType (some 1) fun below _ => do
-    let main ← mkFreshExprSyntheticOpaqueMVar FType
     let below := below[0]
     let valueNew     ← replaceIndPredRecApps recFnName recArgInfo motive value
     let Farg         ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 5e0c3ea0da..209a948946 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -20,7 +20,7 @@ structure EqnInfo extends EqnInfoCore where
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
+  let some (_, lhs, _) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
   if lhs.isAppOf ``WellFounded.fix then
     return mvarId
   else
@@ -143,7 +143,7 @@ private def tryToFoldLHS? (info : EqnInfo) (us : List Level) (fixedPrefix : Arra
 -/
 private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId) : MetaM (List Level × Array Expr) := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) := target.eq? | unreachable!
+  let some (_, lhs, _) := target.eq? | unreachable!
   let lhsArgs := lhs.getAppArgs
   if lhsArgs.size < info.fixedPrefixSize || !lhs.getAppFn matches .const .. then
     throwError "failed to generate equational theorem for '{declName}', unexpected number of arguments in the equation left-hand-side\n{mvarId}"
diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
index 3a2ef060c4..b36ff360c8 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
@@ -62,7 +62,7 @@ partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : Met
   let mut arities := #[]
   let mut modified := false
   for preDef in preDefs do
-    let (preDefNew, arity, modifiedCurr) ← lambdaTelescope preDef.value fun xs body => do
+    let (preDefNew, arity, modifiedCurr) ← lambdaTelescope preDef.value fun xs _ => do
       if xs.size == fixedPrefix then
         throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
       let arity := xs.size
@@ -93,7 +93,6 @@ partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : Met
   for i in [:preDefs.size] do
     let preDef := preDefs[i]
     let preDefNew := preDefsNew[i]
-    let arity := arities[i]
     let valueNew ← lambdaTelescope preDef.value fun xs body => do
       let ys : Array Expr := xs[:fixedPrefix]
       let xs : Array Expr := xs[fixedPrefix:]
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 0df39f1dfe..468117cd19 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -30,7 +30,7 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
   go 0 mvarId fvarId #[]
 
 private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
-  let varNames ← lambdaTelescope preDef.value fun xs body => do
+  let varNames ← lambdaTelescope preDef.value fun xs _ => do
     let mut varNames ← xs.mapM fun x => return (← getLocalDecl x.fvarId!).userName
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size] "too many variable names"
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 1fea084fae..f3d4a12771 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -108,7 +108,6 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
   let mut elseElemStx? := none
   for elementStx in elementStxs do
     let declStx := elementStx[0]
-    let vars := elementStx[1].getArgs
     if declStx.isIdent then
       let declSuffix := declStx.getId
       if alreadyFound.contains declSuffix then
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 01ef9e8853..f36b176449 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -50,10 +50,10 @@ private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (
 private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
   logInfo (← mkHeader' kind id levelParams type isUnsafe)
 
-private def printQuot (kind : QuotKind) (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do
+private def printQuot (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do
   printAxiomLike "Quotient primitive" id levelParams type
 
-private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (numIndices : Nat) (type : Expr)
+private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
   let mut m ← mkHeader' "inductive" id levelParams type isUnsafe
   m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
@@ -69,11 +69,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
   | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
   | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
-  | ConstantInfo.quotInfo  { kind := kind, levelParams := us, type := t, .. } => printQuot kind id us t
+  | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
-  | ConstantInfo.inductInfo { levelParams := us, numParams := numParams, numIndices := numIndices, type := t, ctors := ctors, isUnsafe := u, .. } =>
-    printInduct id us numParams numIndices t ctors u
+  | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
+    printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 4595f10d32..0c34c45801 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -25,7 +25,7 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
       if !e.isIdent || !e.getId.isAtomic then
         return ← withFreshMacroScope do
           let a ← `(a)
-          modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))
+          modify (fun _ stx => (`(let $a:ident := $e; $stx) : TermElabM _))
           pure <| stx.setArg 2 a
     return Syntax.node i k (← args.mapM floatOutAntiquotTerms)
   | stx => pure stx
@@ -260,7 +260,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
   let pat := alt.fst.head!
   let unconditionally (rhsFn) := pure {
     check := unconditional,
-    doMatch := fun yes no => yes [],
+    doMatch := fun yes _ => yes [],
     onMatch := fun taken => covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (match taken with | unconditional => true | _ => false)
   }
   -- quotation pattern
@@ -438,7 +438,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
 private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Array Syntax × Alt)
   -- NOTE: new macro scope so that introduced bindings do not collide
   | (pats, rhs) => do
-    if let `($_:ident $[ $args:ident]*) := rhs then
+    if let `($_:ident $[ $_:ident]*) := rhs then
       -- looks simple enough/created by this function, skip
       return (floatedLetDecls, (pats, rhs))
     withFreshMacroScope do
@@ -460,7 +460,6 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
    pure Syntax.missing
   | discr::discrs, alt::alts    => do
     let info ← getHeadInfo alt
-    let pat  := alt.1.head!
     let alts ← (alt::alts).mapM fun alt => return ((← getHeadInfo alt).onMatch info.check, alt)
     let mut yesAlts           := #[]
     let mut undecidedAlts     := #[]
@@ -507,7 +506,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
   match stx with
   | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     if !patss.any (·.any (fun
-      | `($id@$pat) => pat.isQuot
+      | `($_@$pat) => pat.isQuot
       | pat         => pat.isQuot)) then
       -- no quotations => fall back to regular `match`
       throwUnsupportedSyntax
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 39fe868744..97678282f8 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -195,7 +195,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
 
   If the expected type is available and it is a structure, then we use it.
   Otherwise, we use the type of the first source. -/
-private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
+private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
   tryPostponeIfNoneOrMVar expectedType?
   let useSource : Unit → TermElabM Name := fun _ => do
     match sourceView, expectedType? with
@@ -378,7 +378,7 @@ def Struct.setParams (s : Struct) (ps : Array (Name × Expr)) : Struct :=
 
 private def expandCompositeFields (s : Struct) : Struct :=
   s.modifyFields fun fields => fields.map fun field => match field with
-    | { lhs := FieldLHS.fieldName ref (Name.str Name.anonymous _ _) :: rest, .. } => field
+    | { lhs := FieldLHS.fieldName _ (Name.str Name.anonymous _ _) :: _, .. } => field
     | { lhs := FieldLHS.fieldName ref n@(Name.str _ _ _) :: rest, .. } =>
       let newEntries := n.components.map <| FieldLHS.fieldName ref
       { field with lhs := newEntries ++ rest }
@@ -472,7 +472,6 @@ mutual
 
   private partial def groupFields (s : Struct) : TermElabM Struct := do
     let env ← getEnv
-    let fieldNames := getStructureFields env s.structName
     withRef s.ref do
     s.modifyFieldsM fun fields => do
       let fieldMap ← mkFieldMap fields
@@ -742,7 +741,7 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
         else
           return none
     else
-      if let some (_, param) := struct.params.find? fun (paramName, param) => paramName == n then
+      if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then
         -- Recall that we did not use to have support for parameter propagation here.
         if (← isDefEq (← inferType param) d) then
           mkDefaultValueAux? struct (b.instantiate1 param)
@@ -864,7 +863,7 @@ def propagate (struct : Struct) : TermElabM Unit :=
 end DefaultFields
 
 private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
-  let structName ← getStructName stx expectedType? source
+  let structName ← getStructName expectedType? source
   let struct ← liftMacroM <| mkStructView stx structName source
   let struct ← expandStruct struct
   trace[Elab.struct] "{struct}"
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index f252c774b3..dd72ee479d 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -293,8 +293,8 @@ private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fi
     (where `toGrandparent` is not a field of the current structure). -/
     let visit (e : Expr) : MetaM TransformStep := do
       if let Expr.const subProjName .. := e.getAppFn then
-        if let some { ctorName, numParams, .. } ← getProjectionFnInfo? subProjName then
-          let Name.str subStructName subFieldName .. := subProjName
+        if let some { numParams, .. } ← getProjectionFnInfo? subProjName then
+          let Name.str _ subFieldName .. := subProjName
             | throwError "invalid projection name {subProjName}"
           let args := e.getAppArgs
           if let some major := args.get? numParams then
@@ -374,7 +374,6 @@ where
     match e with
     | Expr.lam n d b c =>
       if c.binderInfo.isExplicit then
-        let fieldName := n
         match fieldMap.find? n with
         | none => failed
         | some val =>
@@ -543,7 +542,7 @@ where
                                       kind := StructFieldKind.newField }
             go (i+1) defaultValsOverridden infos
       | some info =>
-        let updateDefaultValue (fromParent : Bool) : TermElabM α := do
+        let updateDefaultValue : TermElabM α := do
           match view.value? with
           | none       => throwError "field '{view.name}' has been declared in parent structure"
           | some valStx =>
@@ -563,8 +562,8 @@ where
         match info.kind with
         | StructFieldKind.newField    => throwError "field '{view.name}' has already been declared"
         | StructFieldKind.subobject   => throwError "unexpected subobject field reference" -- improve error message
-        | StructFieldKind.copiedField => updateDefaultValue false
-        | StructFieldKind.fromParent  => updateDefaultValue true
+        | StructFieldKind.copiedField => updateDefaultValue
+        | StructFieldKind.fromParent  => updateDefaultValue
     else
       k infos
 
@@ -789,7 +788,6 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
     if field.declName == view.ctor.declName then
       throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
     addAuxDeclarationRanges field.declName field.ref field.ref
-  let numExplicitParams := view.params.size
   let type ← Term.elabType view.type
   unless validStructType type do throwErrorAt view.type "expected Type"
   withRef view.ref do
@@ -799,7 +797,6 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
     let u ← getResultUniverse type
     let univToInfer? ← shouldInferResultUniverse u
     withUsed view.scopeVars view.params fieldInfos fun scopeVars => do
-      let numParams := scopeVars.size + numExplicitParams
       let fieldInfos ← levelMVarToParam scopeVars view.params fieldInfos univToInfer?
       let type ← withRef view.ref do
         if univToInfer?.isSome then
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 430383b132..b6756e44a7 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -343,7 +343,7 @@ def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
   given == expected || given == expected ++ `antiquot
 
 def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
-  | `(matchAltExpr| | $pat:term => $rhs) => do
+  | `(matchAltExpr| | $pat:term => $_) => do
     if !pat.isQuot then
       throwUnsupportedSyntax
     let quoted := getQuotContent pat
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 369fe73445..5e45c5a177 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -303,7 +303,6 @@ mutual
 
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
     /- Recall, `tacticCode` is the whole `by ...` expression. -/
-    let byTk := tacticCode[0]
     let code := tacticCode[1]
     modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
     let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 93c79a90a7..9c75cf3b15 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -161,7 +161,6 @@ mutual
     let rec loop
       | []    => throwErrorAt stx "tactic '{stx.getKind}' has not been implemented"
       | m::ms => do
-        let scp ← getCurrMacroScope
         try
           withReader ({ · with elaborator := m.declName }) do
             withTacticInfoContext stx do
@@ -283,7 +282,7 @@ def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
-  let (mvarId :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
+  let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun _ => { goals := mvarIds ++ mvarIds' }
 
 /-- Return the first goal. -/
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 387025cb2d..6639bb017d 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -161,7 +161,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 @[builtinTactic choice] def evalChoice : Tactic := fun stx =>
   evalChoiceAux stx.getArgs 0
 
-@[builtinTactic skip] def evalSkip : Tactic := fun stx => pure ()
+@[builtinTactic skip] def evalSkip : Tactic := fun _ => pure ()
 
 @[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do
   addCompletionInfo <| CompletionInfo.tactic stx (← getGoals)
@@ -171,24 +171,22 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   if (← try evalTactic tactic; pure true catch _ => pure false) then
     throwError "tactic succeeded"
 
-@[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do
+@[builtinTactic traceState] def evalTraceState : Tactic := fun _ => do
   let gs ← getUnsolvedGoals
   addRawTrace (goalsToMessageData gs)
 
 @[builtinTactic traceMessage] def evalTraceMessage : Tactic := fun stx => do
   match stx[1].isStrLit? with
   | none     => throwIllFormedSyntax
-  | some msg =>
-    let gs ← getUnsolvedGoals
-    withRef stx[0] <| addRawTrace msg
+  | some msg => withRef stx[0] <| addRawTrace msg
 
-@[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun _ =>
   liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure []
 
-@[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun _ =>
   liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure []
 
-@[builtinTactic Lean.Parser.Tactic.refl] def evalRefl : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.refl] def evalRefl : Tactic := fun _ =>
   liftMetaTactic fun mvarId => do Meta.refl mvarId; pure []
 
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
@@ -257,7 +255,7 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
   | `(tactic| subst $hs*) => forEachVar hs Meta.subst
   | _                     => throwUnsupportedSyntax
 
-@[builtinTactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
 /--
@@ -329,7 +327,7 @@ private def getCaseGoals (tag : Syntax) : TacticM (MVarId × List MVarId) := do
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «case'»] def evalCase' : Tactic
-  | stx@`(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => do
     let (g, gs) ← getCaseGoals tag
     let g ← renameInaccessibles g hs
     let mvarTag ← getMVarTag g
@@ -342,7 +340,7 @@ private def getCaseGoals (tag : Syntax) : TacticM (MVarId × List MVarId) := do
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
-  | stx@`(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
+  | `(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 2e8360c972..d9145e5b93 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -71,11 +71,11 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
   liftMetaTactic1 fun mvarId => do
     replaceTargetDefEq mvarId (mkLHSGoal (← mkEq lhs' rhs))
 
-@[builtinTactic Lean.Parser.Tactic.Conv.whnf] def evalWhnf : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.Conv.whnf] def evalWhnf : Tactic := fun _ =>
    withMainContext do
      changeLhs (← whnf (← getLhs))
 
-@[builtinTactic Lean.Parser.Tactic.Conv.reduce] def evalReduce : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.Conv.reduce] def evalReduce : Tactic := fun _ =>
    withMainContext do
      changeLhs (← reduce (← getLhs))
 
@@ -108,7 +108,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 def remarkAsConvGoal : TacticM Unit := do
   let newGoals ← (← getUnsolvedGoals).mapM fun mvarId => withMVarContext mvarId do
     let target ← getMVarType mvarId
-    if let some (_, lhs, rhs) ← matchEq? target then
+    if let some (_, _, rhs) ← matchEq? target then
       if rhs.getAppFn.isMVar then
         replaceTargetDefEq mvarId (mkLHSGoal target)
       else
diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 0c52031ab2..9a8988e913 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -59,7 +59,7 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) :=
     else
       throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
 
-@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
+@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
    replaceMainGoal (← congr (← getMainGoal))
 
 private def selectIdx (tacticName : String) (mvarIds : List MVarId) (i : Int) : TacticM Unit := do
@@ -73,11 +73,11 @@ private def selectIdx (tacticName : String) (mvarIds : List MVarId) (i : Int) :
       return ()
   throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"
 
-@[builtinTactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun stx => do
+@[builtinTactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
    let mvarIds ← congr (← getMainGoal)
    selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
 
-@[builtinTactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun stx => do
+@[builtinTactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
    let mvarIds ← congr (← getMainGoal)
    selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
 
@@ -95,7 +95,7 @@ private def selectIdx (tacticName : String) (mvarIds : List MVarId) (i : Int) :
 private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :=
    withMVarContext mvarId do
      let userNames := if let some userName := userName? then [userName] else []
-     let (lhs, rhs) ← getLhsRhsCore mvarId
+     let (lhs, _) ← getLhsRhsCore mvarId
      let lhs ← instantiateMVars lhs
      if lhs.isForall then
        let [mvarId, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result"
diff --git a/src/Lean/Elab/Tactic/Conv/Simp.lean b/src/Lean/Elab/Tactic/Conv/Simp.lean
index 76cdb6fee6..a3fdedbb96 100644
--- a/src/Lean/Elab/Tactic/Conv/Simp.lean
+++ b/src/Lean/Elab/Tactic/Conv/Simp.lean
@@ -22,7 +22,7 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let result ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
   applySimpResult result
 
-@[builtinTactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun stx => withMainContext do
+@[builtinTactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
   applySimpResult (← Split.simpMatch (← getLhs))
 
 end Lean.Elab.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 770fcfce96..1104bb4828 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -203,7 +203,7 @@ def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
   | `(tactic| apply $e) => evalApplyLikeTactic Meta.apply e
   | _ => throwUnsupportedSyntax
 
-@[builtinTactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun _ =>
   withMainContext do
     let mvarIds'  ← Meta.constructor (← getMainGoal)
     Term.synthesizeSyntheticMVarsNoPostponing
@@ -272,7 +272,7 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
   return expectedType
 
-@[builtinTactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
   closeMainGoalUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
@@ -295,7 +295,7 @@ private def mkNativeAuxDecl (baseName : Name) (type val : Expr) : TermElabM Name
   compileDecl decl
   pure auxName
 
-@[builtinTactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx =>
+@[builtinTactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
   closeMainGoalUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 5f9cdb38d5..af3e0f6c97 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -443,7 +443,6 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
         ElimApp.mkElimApp elimInfo targets tag
       trace[Elab.induction] "elimApp: {result.elimApp}"
       let elimArgs := result.elimApp.getAppArgs
-      let motiveType ← inferType elimArgs[elimInfo.motivePos]
       ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
       let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
       assignExprMVar mvarId result.elimApp
diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index d693d317be..3eb666ad08 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -27,7 +27,7 @@ private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Uni
     | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; return []
     | Meta.InjectionResult.subgoal mvarId' _ unusedIds => checkUnusedIds mvarId unusedIds; return [mvarId']
 
-@[builtinTactic «injections»] def evalInjections : Tactic := fun stx => do
+@[builtinTactic «injections»] def evalInjections : Tactic := fun _ => do
   liftMetaTactic fun mvarId => do
     match (← Meta.injections mvarId) with
     | none => return []
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index c6dad5da9d..feda6e7650 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -30,7 +30,6 @@ def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Re
 def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
   let lbrak := rwRulesSeqStx[0]
   let rules := rwRulesSeqStx[1].getArgs
-  let rbrak := rwRulesSeqStx[2]
   -- show initial state up to (incl.) `[`
   withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
   let numRules := (rules.size + 1) / 2
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 7e94f7c99f..450207edc0 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -595,7 +595,7 @@ def throwTypeMismatchError (header? : Option String) (expectedType : Expr) (eTyp
   -/
   match f? with
   | none   => throwError "{← mkTypeMismatchError header? e eType expectedType}{extraMsg}"
-  | some f => Meta.throwAppTypeMismatch f e extraMsg
+  | some f => Meta.throwAppTypeMismatch f e
 
 def withoutMacroStackAtErr (x : TermElabM α) : TermElabM α :=
   withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := pp.macroStack.set ctx.options false }) x
@@ -951,9 +951,8 @@ def withSavedContext (savedCtx : SavedContext) (x : TermElabM α) : TermElabM α
 private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   trace[Elab.postpone] "{stx} : {expectedType?}"
   let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque
-  let ctx ← read
   registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext))
-  pure mvar
+  return mvar
 
 def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
   return (← get).syntheticMVars.find? fun d => d.mvarId == mvarId
@@ -1103,8 +1102,8 @@ private def isExplicitApp (stx : Syntax) : Bool :=
   Example: `fun {α} (a : α) => a` -/
 private def isLambdaWithImplicit (stx : Syntax) : Bool :=
   match stx with
-  | `(fun $binders* => $body) => binders.any fun b => b.isOfKind ``Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
-  | _                         => false
+  | `(fun $binders* => $_) => binders.any fun b => b.isOfKind ``Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
+  | _                      => false
 
 private partial def dropTermParens : Syntax → Syntax := fun stx =>
   match stx with
@@ -1130,8 +1129,8 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($_ : $type)) => true
-  | _               => false
+  | `(($_ : $_)) => true
+  | _            => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
   annotation? `noImplicitLambda type |>.isSome
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 0d070e6622..ab86a7b9ad 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -453,7 +453,7 @@ def TagDeclarationExtension := SimplePersistentEnvExtension Name NameSet
 def mkTagDeclarationExtension (name : Name) : IO TagDeclarationExtension :=
   registerSimplePersistentEnvExtension {
     name          := name,
-    addImportedFn := fun as => {},
+    addImportedFn := fun _ => {},
     addEntryFn    := fun s n => s.insert n,
     toArrayFn     := fun es => es.toArray.qsort Name.quickLt
   }
@@ -482,7 +482,7 @@ def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name ×
 def mkMapDeclarationExtension [Inhabited α] (name : Name) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
     name          := name,
-    addImportedFn := fun as => {},
+    addImportedFn := fun _ => {},
     addEntryFn    := fun s n => s.insert n.1 n.2 ,
     toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
   }
diff --git a/src/Lean/Eval.lean b/src/Lean/Eval.lean
index 062348f4f8..b557dd2e18 100644
--- a/src/Lean/Eval.lean
+++ b/src/Lean/Eval.lean
@@ -16,7 +16,7 @@ class MetaEval (α : Type u) where
   eval : Environment → Options → α → (hideUnit : Bool) → IO Environment
 
 instance {α : Type u} [Eval α] : MetaEval α :=
-  ⟨fun env opts a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩
+  ⟨fun env _ a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩
 
 def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
   IO.FS.withIsolatedStreams (MetaEval.eval env opts a false |>.toBaseIO)
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 05f3c49c28..86ee113616 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -123,7 +123,6 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
         | Expr.const c _ _ =>
           if c != df.valueTypeName then throwError "unexpected type at '{declName}', '{df.valueTypeName}' expected"
           else
-            let env ← getEnv
             /- builtin_initialize @addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(declName) $(mkConst declName) -/
             let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, toExpr declName, mkConst declName]
             declareBuiltin declName val
diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean
index bdef55613e..e348263996 100644
--- a/src/Lean/Meta/ACLt.lean
+++ b/src/Lean/Meta/ACLt.lean
@@ -110,14 +110,6 @@ where
     -- See main function
     | Expr.mdata ..         => unreachable!
 
-  lex (a b : Expr) : MetaM Bool :=
-    if a.ctorWeight < b.ctorWeight then
-      return true
-    else if a.ctorWeight > b.ctorWeight then
-      return false
-    else
-      lexSameCtor a b
-
   allChildrenLt (a b : Expr) : MetaM Bool :=
     match a with
     | Expr.proj _ _ e ..    => lt e b
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 1704abe160..5485e50996 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -487,7 +487,7 @@ def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
     setMCtx sNew.mctx
     modifyThe Core.State fun s => { s with ngen := sNew.ngen, nextMacroScope := sNew.nextMacroScope }
     pure e
-  | EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) sNew => do
+  | EStateM.Result.error (.revertFailure ..) sNew => do
     setMCtx sNew.mctx
     modifyThe Core.State fun s => { s with ngen := sNew.ngen, nextMacroScope := sNew.nextMacroScope }
     throwError "failed to create binder due to failure when reverting variable dependencies"
@@ -758,7 +758,7 @@ mutual
 
   private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=
     withReducible do -- when testing whether a type is a type class, we only unfold reducible constants.
-      forallTelescopeReducingAux type none fun xs type => do
+      forallTelescopeReducingAux type none fun _ type => do
         let env ← getEnv
         match type.getAppFn with
         | Expr.const c _ _ => do
@@ -1010,7 +1010,6 @@ def withLocalInstances (decls : List LocalDecl) : n α → n α :=
 
 private def withExistingLocalDeclsImp (decls : List LocalDecl) (k : MetaM α) : MetaM α := do
   let ctx ← read
-  let numLocalInstances := ctx.localInstances.size
   let lctx := decls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) ctx.lctx
   withReader (fun ctx => { ctx with lctx := lctx }) do
     withLocalInstancesImp decls k
@@ -1165,7 +1164,7 @@ instance : Alternative MetaM where
   orElse  := Meta.orElse
 
 @[inline] private def orelseMergeErrorsImp (x y : MetaM α)
-    (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)
+    (mergeRef : Syntax → Syntax → Syntax := fun r₁ _ => r₁)
     (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ m₂) : MetaM α := do
   let env  ← getEnv
   let mctx ← getMCtx
@@ -1188,7 +1187,7 @@ instance : Alternative MetaM where
   The default `mergeRef` uses the `ref` (position information) for the first message.
   The default `mergeMsg` combines error messages using `Format.line ++ Format.line` as a separator. -/
 @[inline] def orelseMergeErrors [MonadControlT MetaM m] [Monad m] (x y : m α)
-    (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)
+    (mergeRef : Syntax → Syntax → Syntax := fun r₁ _ => r₁)
     (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ Format.line ++ m₂) : m α := do
   controlAt MetaM fun runInBase => orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg
 
diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean
index 0ee8e05b77..172547c910 100644
--- a/src/Lean/Meta/CasesOn.lean
+++ b/src/Lean/Meta/CasesOn.lean
@@ -82,7 +82,6 @@ def CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := fa
     return { c with us, motive, alts, remaining }
 where
   updateAlts (argType : Expr) (auxType : Expr) : MetaM (Array Expr) := do
-    let indName := c.declName.getPrefix
     let mut auxType := auxType
     let mut altsNew := #[]
     let mut refined := false
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 682c81bacf..29caa140c0 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -125,7 +125,7 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageDat
     let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
     return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
 
-def throwAppTypeMismatch {α} (f a : Expr) (extraMsg : MessageData := Format.nil) : MetaM α := do
+def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   let (expectedType, binfo) ← getFunctionDomain f
   let mut e := mkApp f a
   unless binfo.isExplicit do
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index ab2dfeb8ea..42de3cdd28 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -152,12 +152,12 @@ def mkNewLevelParam (u : Level) : ClosureM Level := do
   pure $ mkLevelParam p
 
 partial def collectLevelAux : Level → ClosureM Level
-  | u@(Level.succ v _)      => return u.updateSucc! (← visitLevel collectLevelAux v)
-  | u@(Level.max v w _)     => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
-  | u@(Level.imax v w _)    => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
-  | u@(Level.mvar mvarId _) => mkNewLevelParam u
-  | u@(Level.param _ _)     => mkNewLevelParam u
-  | u@(Level.zero _)        => pure u
+  | u@(Level.succ v _)   => return u.updateSucc! (← visitLevel collectLevelAux v)
+  | u@(Level.max v w _)  => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
+  | u@(Level.imax v w _) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
+  | u@(Level.mvar ..)    => mkNewLevelParam u
+  | u@(Level.param ..)   => mkNewLevelParam u
+  | u@(Level.zero _)     => pure u
 
 def collectLevel (u : Level) : ClosureM Level := do
   -- u ← instantiateLevelMVars u
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index d9a88ede66..386d2b902e 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -218,7 +218,7 @@ where
   mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
     try
       let fType ← inferType f
-      forallBoundedTelescope fType kinds.size fun lhss xType => do
+      forallBoundedTelescope fType kinds.size fun lhss _ => do
         if lhss.size != kinds.size then return none
         let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
           if i == kinds.size then
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c549eea44c..ebde6c6ea8 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -52,7 +52,6 @@ where
         checkpointDefEq do
           let args := b.getAppArgs
           let params := args[:ctorVal.numParams].toArray
-          let info? := getStructureInfo? (← getEnv) ctorVal.induct
           for i in [ctorVal.numParams : args.size] do
             let j := i - ctorVal.numParams
             let proj ← mkProjFn ctorVal us params j a
@@ -785,7 +784,7 @@ end CheckAssignment
 namespace CheckAssignmentQuick
 
 partial def check
-    (hasCtxLocals ctxApprox : Bool)
+    (hasCtxLocals : Bool)
     (mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : MVarId) (fvars : Array Expr) (e : Expr) : Bool :=
   let rec visit (e : Expr) : Bool :=
     if !e.hasExprMVar && !e.hasFVar then
@@ -845,7 +844,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
     let hasCtxLocals := fvars.any fun fvar => mvarDecl.lctx.containsFVar fvar
     let ctx ← read
     let mctx ← getMCtx
-    if CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox mctx ctx.lctx mvarDecl mvarId fvars v then
+    if CheckAssignmentQuick.check hasCtxLocals mctx ctx.lctx mvarDecl mvarId fvars v then
       pure (some v)
     else
       let v ← instantiateMVars v
@@ -1495,10 +1494,6 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
 
 -- Both `t` and `s` are terms of the form `?m ...`
 private partial def isDefEqQuickMVarMVar (t s : Expr) : MetaM LBool := do
-  let tFn := t.getAppFn
-  let sFn := s.getAppFn
-  let tMVarDecl ← getMVarDecl tFn.mvarId!
-  let sMVarDecl ← getMVarDecl sFn.mvarId!
   if s.isMVar && !t.isMVar then
      /- Solve `?m t =?= ?n` by trying first `?n := ?m t`.
         Reason: this assignment is precise. -/
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 67fd64916e..2b0331a726 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -154,7 +154,7 @@ where
     let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
     let (_, cnt) ← run <| transform domain fun e => do
       if let some name := e.constName? then
-        if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
+        if let some _ := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
           modify (· + 1)
       return TransformStep.visit e
 
@@ -176,7 +176,6 @@ where
         if let some name := f.constName? then
           if let some idx := ctx.typeInfos.findIdx?
             fun indVal => indVal.name == name then
-            let indVal := ctx.typeInfos[idx]
             let hApp := mkAppN binder xs
             let t :=
               mkAppN vars.indVal[idx] $
@@ -257,7 +256,7 @@ partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) :
   let ms ← induction m vars
   let ms ← applyCtors ms
   let maxDepth := maxBackwardChainingDepth.get $ ←getOptions
-  ms.forM (closeGoal vars maxDepth)
+  ms.forM (closeGoal maxDepth)
   instantiateMVars main
 where
   intros (m : MVarId) : MetaM (MVarId × BrecOnVariables) := do
@@ -270,7 +269,7 @@ where
 
   applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
     match (← vars.indHyps.findSomeM?
-      fun ih => do try pure <| some <| (←apply m $ mkFVar ih) catch ex => pure none) with
+      fun ih => do try pure <| some <| (←apply m $ mkFVar ih) catch _ => pure none) with
     | some goals => pure goals
     | none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
 
@@ -291,11 +290,11 @@ where
     apply m recursor
 
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
-    let mss ← ms.toArray.mapIdxM fun idx m => do
+    let mss ← ms.toArray.mapIdxM fun _ m => do
       let m ← introNPRec m
       (← getMVarType m).withApp fun below args =>
       withMVarContext m do
-        args.back.withApp fun ctor ctorArgs => do
+        args.back.withApp fun ctor _ => do
         let ctorName := ctor.constName!.updatePrefix below.constName!
         let ctor := mkConst ctorName below.constLevels!
         let ctorInfo ← getConstInfoCtor ctorName
@@ -307,7 +306,7 @@ where
   introNPRec (m : MVarId) : MetaM MVarId := do
     if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else return m
 
-  closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
+  closeGoal (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
     unless (← isExprMVarAssigned m) do
       let m ← introNPRec m
       unless (← backwardsChaining m maxDepth) do
@@ -358,7 +357,6 @@ where
 partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do
   let ctorInfo ← getConstInfoCtor ctorName
   let belowCtorInfo ← getConstInfoCtor (ctorName.updatePrefix $ ctorInfo.induct ++ `below)
-  let belowInductInfo ← getConstInfoInduct belowCtorInfo.induct
   forallTelescopeReducing ctorInfo.type fun xs _ => do
   loop xs belowCtorInfo.type #[] 0 0
 
@@ -376,7 +374,7 @@ where
       let rest ← instantiateForall rest #[x]
       loop xs rest (belowIndices.push yIdx) (xIdx + 1) (yIdx + 1)
     else
-      forallBoundedTelescope rest (some 1) fun ys rest =>
+      forallBoundedTelescope rest (some 1) fun _ rest =>
       loop xs rest belowIndices xIdx (yIdx + 1)
 
 private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Name × Expr := do
@@ -407,7 +405,7 @@ partial def mkBelowMatcher
     (below : Expr)
     (idx : Nat) : MetaM $ Expr × MetaM Unit := do
   let mkMatcherInput ← getMkMatcherInputInContext matcherApp
-  let (indName, belowType, motive, matchType) ←
+  let (indName, _, motive, matchType) ←
     forallBoundedTelescope mkMatcherInput.matchType mkMatcherInput.numDiscrs fun xs t => do
     let (indName, belowType) ← belowType belowMotive xs idx
     let matchType ←
@@ -442,7 +440,6 @@ partial def mkBelowMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.
   check res.matcher
-  let args := #[motive] ++ matcherApp.discrs.push below ++ alts
   let newApp := mkApp res.matcher motive
   let newApp := mkAppN newApp $ matcherApp.discrs.push below
   let newApp := mkAppN newApp alts
@@ -506,7 +503,6 @@ where
       return (additionalFVars, Pattern.as varId p hId)
     | Pattern.var varId =>
       let var := mkFVar varId
-      (←inferType var).withApp fun ind args => do
       let (_, tgtType) ← belowType belowMotive #[var] 0
       withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do
       let localDecl ← getFVarLocalDecl h
@@ -524,7 +520,7 @@ where
         let belowFieldExpr ← belowField.toExpr
         let belowCtor := mkApp belowCtor belowFieldExpr
         let patTy ← inferType belowFieldExpr
-        patTy.withApp fun f args => do
+        patTy.withApp fun f _ => do
         let constName := f.constName?
         if constName == indName then
           let (fvars, transformedField) ← convertToBelow indName belowField
@@ -560,7 +556,7 @@ where
 def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
   xs.findSomeM? fun x => do
   let xTy ← inferType x
-  xTy.withApp fun f args =>
+  xTy.withApp fun f _ =>
   match f.constName?, xs.indexOf? x with
   | some name, some idx => do
     if (← isInductivePredicate name) then
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index cbe36f8298..dcfbfc521a 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -47,7 +47,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
       trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
       let thenH := (thenSubst.get thenH).fvarId!
       trace[Meta] "searching for decl"
-      let decl ← getLocalDecl thenH
+      let _ ← getLocalDecl thenH
       trace[Meta] "found decl"
     let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
     pure (thenSubgoal, elseSubgoal)
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 355ed45524..129127f959 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -261,7 +261,6 @@ def assign (fvarId : FVarId) (v : Expr) : M Bool := do
     trace[Meta.Match.unify] "assign occurs check failed, {mkFVar fvarId} := {v}"
     return false
   else
-    let ctx ← read
     if (← isAltVar fvarId) then
       trace[Meta.Match.unify] "{mkFVar fvarId} := {v}"
       modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
@@ -300,8 +299,6 @@ private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option
 
 private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=
   withExistingLocalDecls alt.fvarDecls do
-    let env ← getEnv
-    let ldecl ← getLocalDecl fvarId
     let expectedType ← inferType (mkFVar fvarId)
     let expectedType ← whnfD expectedType
     let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType
@@ -383,7 +380,6 @@ private def throwCasesException (p : Problem) (ex : Exception) : MetaM α := do
 
 private def processConstructor (p : Problem) : MetaM (Array Problem) := do
   trace[Meta.Match.match] "constructor step"
-  let env ← getEnv
   match p.vars with
   | []      => unreachable!
   | x :: xs => do
@@ -627,7 +623,7 @@ private def List.moveToFront [Inhabited α] (as : List α) (i : Nat) : List α :
 private def moveToFront (p : Problem) (i : Nat) : Problem :=
   if i == 0 then
     p
-  else if h : i < p.vars.length then
+  else if i < p.vars.length then
     { p with
       vars := List.moveToFront p.vars i
       alts := p.alts.map fun alt => { alt with patterns := List.moveToFront alt.patterns i }
@@ -841,7 +837,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
   trace[Meta.Match.debug] "motiveType: {motiveType}"
   withLocalDeclD `motive motiveType fun motive => do
   if discrInfos.any fun info => info.hName?.isSome then
-    forallBoundedTelescope matchType numDiscrs fun discrs' matchTypeBody => do
+    forallBoundedTelescope matchType numDiscrs fun discrs' _ => do
     let (mvarType, isEqMask) ← withEqs discrs discrs' discrInfos fun eqs => do
       let mvarType ← mkForallFVars eqs (mkAppN motive discrs')
       let isEqMask ← eqs.mapM fun eq => return (← inferType eq).isEq
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index a91ae33e95..831c7843b7 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -18,7 +18,7 @@ namespace Lean.Meta
   apply `cases xMajor`. -/
 partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do
   let target ← getMVarType mvarId
-  if let some (_, lhs, rhs) ← matchEq? target then
+  if let some (_, lhs, _) ← matchEq? target then
     if let some fvarId ← findFVar? lhs then
       return (← cases mvarId fvarId).map fun s => s.mvarId
   throwError "'casesOnStuckLHS' failed"
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index d09f6379ff..56d96f8724 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -146,7 +146,6 @@ goal from being littered with irrelevant names.
 
 -/
 def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do
-  let lctx ← getLCtx
   if pp.inaccessibleNames.get (← getOptions) then
     -- If `pp.inaccessibleNames == true`, we still must compute `hiddenInaccessibleProp`.
     let hiddenInaccessible ← getInitialHiddenInaccessible (propOnly := true)
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 8b4aa850bd..053b8ed650 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -117,7 +117,7 @@ private partial def getNumParams (xs : Array Expr) (motive : Expr) (i : Nat) : N
   else
     i
 
-private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : Array Expr) (motive : Expr) (motiveArgs : Array Expr)
+private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : Array Expr) (motiveArgs : Array Expr)
     : MetaM (Expr × Nat × Bool) := do
   match majorPos? with
   | some majorPos =>
@@ -207,7 +207,7 @@ private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) :
   forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
     checkMotive declName motive motiveArgs
     let numParams := getNumParams xs motive 0
-    let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs
+    let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motiveArgs
     let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size
     if majorPos < numIndices then
       throwError "invalid user defined recursor '{declName}', indices must occur before major premise"
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index f2bbe18426..eacfa86253 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -118,7 +118,7 @@ where
 partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
   trace[Meta.sizeOf] "recName: {recName}"
   let recInfo : RecursorVal ← getConstInfoRec recName
-  forallTelescopeReducing recInfo.type fun xs type =>
+  forallTelescopeReducing recInfo.type fun xs _ =>
     let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined
     let params := xs[:recInfo.numParams]
     let motiveFVars := xs[recInfo.numParams : recInfo.numParams + recInfo.numMotives]
@@ -180,7 +180,7 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
   ctorName ++ `sizeOf_spec
 
 def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
-  matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo ctorLevels => do
+  matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo _ => do
     let ctorArgs     := ctorApp.getAppArgs
     let ctorFields   := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
     let lemmaName  := mkSizeOfSpecLemmaName ctorInfo.name
@@ -254,7 +254,7 @@ mutual
       mkSizeOfAuxLemma lhs rhs
 
   /-- Construct proof of auxiliary lemma. See `mkSizeOfAuxLemma` -/
-  private partial def mkSizeOfAuxLemmaProof (info : InductiveVal) (lhs rhs : Expr) : M Expr := do
+  private partial def mkSizeOfAuxLemmaProof (info : InductiveVal) (lhs : Expr) : M Expr := do
     let lhsArgs := lhs.getAppArgs
     let sizeOfBaseArgs := lhsArgs[:lhsArgs.size - info.numIndices - 1]
     let indicesMajor := lhsArgs[lhsArgs.size - info.numIndices - 1:]
@@ -309,7 +309,7 @@ mutual
                   let specEq ← whnf (← inferType specLemma)
                   match specEq.eq? with
                   | none => throwFailed
-                  | some (_, rhs, rhsExpanded) =>
+                  | some (_, _, rhsExpanded) =>
                     let lhs_eq_rhsExpanded ← mkMinorProof ys lhs rhsExpanded
                     let rhsExpanded_eq_rhs ← mkEqSymm specLemma
                     mkLambdaFVars ys (← mkEqTrans lhs_eq_rhsExpanded rhsExpanded_eq_rhs)
@@ -363,7 +363,7 @@ mutual
               let eq ← mkEq lhsNew rhsNew
               let thmParams := lhsArgsNew
               let thmType ← mkForallFVars thmParams eq
-              let thmValue ← mkSizeOfAuxLemmaProof info lhsNew rhsNew
+              let thmValue ← mkSizeOfAuxLemmaProof info lhsNew
               let thmValue ← mkLambdaFVars thmParams thmValue
               trace[Meta.sizeOf] "thmValue: {thmValue}"
               addDecl <| Declaration.thmDecl {
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index fbff429ec8..e342e8e447 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -639,7 +639,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) :
 private def preprocessOutParam (type : Expr) : MetaM Expr :=
   forallTelescope type fun xs typeBody => do
     match typeBody.getAppFn with
-    | c@(Expr.const constName us _) =>
+    | c@(Expr.const constName _ _) =>
       let env ← getEnv
       if !hasOutParams env constName then
         return type
diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index 7b1404ef50..ffd304c312 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -168,7 +168,7 @@ where
       | none => return Simp.Step.done { expr := e }
     | e, _ => return Simp.Step.done { expr := e }
 
-@[builtinTactic ac_refl] def ac_refl_tactic : Lean.Elab.Tactic.Tactic := fun stx => do
+@[builtinTactic ac_refl] def ac_refl_tactic : Lean.Elab.Tactic.Tactic := fun _ => do
   let goal ← getMainGoal
   rewriteUnnormalized goal
 
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 06113ce9e8..acb4cca4ba 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -84,7 +84,7 @@ private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MV
       let (nonDeps, deps) ← partitionDependentMVars mvars
       return nonDeps.toList ++ deps.toList
   | ApplyNewGoals.nonDependentOnly => do
-      let (nonDeps, deps) ← partitionDependentMVars mvars
+      let (nonDeps, _) ← partitionDependentMVars mvars
       return nonDeps.toList
   | ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId!
 
@@ -142,7 +142,7 @@ def applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Uni
     let some [] ← observing? do apply mvarId (mkConst ``Eq.refl [← mkFreshLevelMVar])
       | throwTacticEx `refl mvarId msg
 
-def exfalso (mvarId : MVarId) (msg : MessageData := "exfalso failed") : MetaM MVarId :=
+def exfalso (mvarId : MVarId) : MetaM MVarId :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `exfalso
     let target ← instantiateMVars (← getMVarType mvarId)
diff --git a/src/Lean/Meta/Tactic/Cleanup.lean b/src/Lean/Meta/Tactic/Cleanup.lean
index 98c1f1310d..b6f7c25e40 100644
--- a/src/Lean/Meta/Tactic/Cleanup.lean
+++ b/src/Lean/Meta/Tactic/Cleanup.lean
@@ -41,7 +41,7 @@ where
 
   addUsedFVar (fvarId : FVarId) : StateRefT (Bool × FVarIdSet) MetaM Unit := do
     unless (← get).2.contains fvarId do
-      modify fun (modified, s) => (true, s.insert fvarId)
+      modify fun (_, s) => (true, s.insert fvarId)
       addDeps fvarId
 
   /- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set. -/
diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean
index 373038c167..29b6132866 100644
--- a/src/Lean/Meta/Tactic/Constructor.lean
+++ b/src/Lean/Meta/Tactic/Constructor.lean
@@ -29,7 +29,7 @@ def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
     let target ← getMVarType' mvarId
     matchConstStruct target.getAppFn
       (fun _ => throwTacticEx `exists mvarId "target is not an inductive datatype with one constructor")
-      fun ival us cval => do
+      fun _ us cval => do
         if cval.numFields < 2 then
           throwTacticEx `exists mvarId "constructor must have at least two fields"
         let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.numParams]
diff --git a/src/Lean/Meta/Tactic/Delta.lean b/src/Lean/Meta/Tactic/Delta.lean
index ca5d62bcc1..c231d88ecf 100644
--- a/src/Lean/Meta/Tactic/Delta.lean
+++ b/src/Lean/Meta/Tactic/Delta.lean
@@ -31,7 +31,6 @@ def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
 def deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `delta
-    let localDecl ← getLocalDecl fvarId
     changeLocalDecl mvarId fvarId (← deltaExpand (← getMVarType mvarId) p) (checkDefEq := false)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index b3d1f03a01..0eada8cd87 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -138,7 +138,7 @@ builtin_initialize
   registerBuiltinAttribute {
     name  := `eliminator
     descr := "custom eliminator for `cases` and `induction` tactics"
-    add   := fun declName stx attrKind => do
+    add   := fun declName _ attrKind => do
       discard <| addCustomEliminator declName attrKind |>.run {} {}
   }
 
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 289fd10cbb..a6b8ec3a47 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -21,7 +21,6 @@ namespace Lean.Meta
           let tag     ← getMVarTag mvarId
           let type := type.headBeta
           let newMVar ← mkFreshExprSyntheticOpaqueMVar type tag
-          let lctx    ← getLCtx
           let newVal  ← mkLambdaFVars fvars newMVar
           assignExprMVar mvarId newVal
           return (fvars, newMVar.mvarId!)
diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
index 9e31d74f90..0b779b7938 100644
--- a/src/Lean/Meta/Tactic/Replace.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -26,7 +26,7 @@ def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : Meta
     let u        ← getLevel target
     let eq       ← mkEq target targetNew
     let newProof ← mkExpectedTypeHint eqProof eq
-    let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew]
+    let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, newProof, mvarNew]
     assignExprMVar mvarId val
     return mvarNew.mvarId!
 
@@ -47,7 +47,7 @@ def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
       let tag     ← getMVarTag mvarId
       let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag
       let newVal  ← mkExpectedTypeHint mvarNew target
-      assignExprMVar mvarId mvarNew
+      assignExprMVar mvarId newVal
       return mvarNew.mvarId!
 
 /--
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 9f5d96a043..ac985a0ecb 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -925,7 +925,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
         | some thmId => pure { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem thmId }
       let r ← simp type ctx discharge?
       match r.proof? with
-      | some proof => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
+      | some _ => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
         | none => return none
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 972ad1fc55..c053cf80b3 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -145,8 +145,8 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | Expr.mdata _ s _, t => isPerm s t
   | s, Expr.mdata _ t _ => isPerm s t
   | s@(Expr.mvar ..), t@(Expr.mvar ..) => isDefEq s t
-  | Expr.forallE n₁ d₁ b₁ _, Expr.forallE n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
-  | Expr.lam n₁ d₁ b₁ _, Expr.lam n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
+  | Expr.forallE n₁ d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
+  | Expr.lam n₁ d₁ b₁ _, Expr.lam _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
   | Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE _  t₂ v₂ b₂ _ =>
     isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
   | Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => pure (i₁ == i₂) <&&> isPerm b₁ b₂
@@ -158,7 +158,7 @@ private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
     throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"
 
 private partial def shouldPreprocess (type : Expr) : MetaM Bool :=
-  forallTelescopeReducing type fun xs result => do
+  forallTelescopeReducing type fun _ result => do
     if let some (_, lhs, rhs) := result.eq? then
       checkBadRewrite lhs rhs
       return false
@@ -235,7 +235,7 @@ private def checkTypeIsProp (type : Expr) : MetaM Unit :=
 private def mkSimpTheoremCore (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (name? : Option Name) : MetaM SimpTheorem := do
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
-    let (xs, _, type) ← withReducible <| forallMetaTelescopeReducing type
+    let (_, _, type) ← withReducible <| forallMetaTelescopeReducing type
     let type ← whnfR type
     let (keys, perm) ←
       match type.eq? with
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 4bdff6ec13..81c2241816 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -169,12 +169,12 @@ where
         let eqType ← inferType eq
         let altEqType := altEqDecl.type
         match eqType.eq?, altEqType.eq? with
-        | some (_, discr, discrVar), some (_, _ /- discr -/, pattern) =>
+        | some (_, _, discrVar), some (_, _ /- discr -/, pattern) =>
           withLocalDeclD altEqDecl.userName (← mkEq discrVar pattern) fun altEqNew => do
             go (i+1) (altEqsNew.push altEqNew) (subst.push (← mkEqTrans eq altEqNew))
         | _, _ =>
         match eqType.heq?, altEqType.heq? with
-        | some (_, discr, _, discrVar), some (_, _ /- discr -/, _, pattern) =>
+        | some (_, _, _, discrVar), some (_, _ /- discr -/, _, pattern) =>
           withLocalDeclD altEqDecl.userName (← mkHEq discrVar pattern) fun altEqNew => do
             go (i+1) (altEqsNew.push altEqNew) (subst.push (← mkHEqTrans eq altEqNew))
         | _, _ =>
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index bacf343a41..5b869108fd 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -32,7 +32,6 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
         let mctx ← getMCtx
         if mctx.exprDependsOn b aFVarId then
           throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"
-        let aLocalDecl ← getLocalDecl aFVarId
         let (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true
         trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}"
         let (twoVars, mvarId) ← introNP mvarId 2
@@ -145,9 +144,9 @@ partial def subst (mvarId : MVarId) (h : FVarId) : MetaM MVarId :=
   withMVarContext mvarId do
     let localDecl ← getLocalDecl h
     match (← matchEq? localDecl.type) with
-    | some (_, lhs, rhs) => substEq mvarId h
+    | some _ => substEq mvarId h
     | none => match (← matchHEq? localDecl.type) with
-      | some (_, lhs, _, rhs) =>
+      | some _ =>
         let (h', mvarId') ← heqToEq mvarId h
         if mvarId == mvarId' then
           findEq mvarId h
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 839a8df0e7..b9cb8cd95b 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -27,7 +27,7 @@ def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do
 def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr :=
   mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
-def throwTacticEx {α} (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ref := Syntax.missing) : MetaM α :=
+def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α :=
   if msg.isEmpty then
     throwError "tactic '{tacticName}' failed\n{mvarId}"
   else
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index 0ec583f997..d5dc31eb70 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -31,8 +31,8 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
     (pre   : Expr → m TransformStep := fun e => return TransformStep.visit e)
     (post  : Expr → m TransformStep := fun e => return TransformStep.done e)
     : m Expr :=
-  let inst : STWorld IO.RealWorld m := ⟨⟩
-  let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
+  let _ : STWorld IO.RealWorld m := ⟨⟩
+  let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
@@ -67,8 +67,8 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
     (post  : Expr → m TransformStep := fun e => return TransformStep.done e)
     (usedLetOnly := false)
     : m Expr := do
-  let inst : STWorld IO.RealWorld m := ⟨⟩
-  let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
+  let _ : STWorld IO.RealWorld m := ⟨⟩
+  let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 77a657181a..098a977a0d 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -58,7 +58,7 @@ where
       let p ← decodeConstraint e
       return { pattern := p, constraints := cs.toList }
 
-private partial def validateHint (declName : Name) (hint : UnificationHint) : MetaM Unit := do
+private partial def validateHint (hint : UnificationHint) : MetaM Unit := do
   hint.constraints.forM fun c => do
     unless (← isDefEq c.lhs c.rhs) do
       throwError "invalid unification hint, failed to unify constraint left-hand-side{indentExpr c.lhs}\nwith right-hand-side{indentExpr c.rhs}"
@@ -76,7 +76,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit :=
       | Except.error msg => throwError msg
       | Except.ok hint =>
         let keys ← DiscrTree.mkPath hint.pattern.lhs
-        validateHint declName hint
+        validateHint hint
         unificationHintExtension.add { keys := keys, val := declName } kind
 
 builtin_initialize
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index e1cb46f3c0..c94a451e2f 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -225,7 +225,7 @@ private def reduceQuotRec (recVal  : QuotVal) (recLvls : List Level) (recArgs :
    =========================== -/
 
 mutual
-  private partial def isRecStuck? (recVal : RecursorVal) (recLvls : List Level) (recArgs : Array Expr) : MetaM (Option MVarId) :=
+  private partial def isRecStuck? (recVal : RecursorVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
     if recVal.k then
       -- TODO: improve this case
       return none
@@ -238,7 +238,7 @@ mutual
       else
         return none
 
-  private partial def isQuotRecStuck? (recVal : QuotVal) (recLvls : List Level) (recArgs : Array Expr) : MetaM (Option MVarId) :=
+  private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
     let process? (majorPos : Nat) : MetaM (Option MVarId) :=
       if h : majorPos < recArgs.size then do
         let major := recArgs.get ⟨majorPos, h⟩
@@ -264,12 +264,12 @@ mutual
     | Expr.app f .. =>
       let f := f.getAppFn
       match f with
-      | Expr.mvar mvarId _       => return some mvarId
-      | Expr.const fName fLvls _ =>
+      | Expr.mvar mvarId _   => return some mvarId
+      | Expr.const fName _ _ =>
         let cinfo? ← getConstNoEx? fName
         match cinfo? with
-        | some $ ConstantInfo.recInfo recVal  => isRecStuck? recVal fLvls e.getAppArgs
-        | some $ ConstantInfo.quotInfo recVal => isQuotRecStuck? recVal fLvls e.getAppArgs
+        | some $ ConstantInfo.recInfo recVal  => isRecStuck? recVal e.getAppArgs
+        | some $ ConstantInfo.quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
         | _                                => return none
       | Expr.proj _ _ e _ => getStuckMVar? (← whnf e)
       | _ => return none
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 7cb628afae..67e745fb1f 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -827,7 +827,6 @@ def collectForwardDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert :
       -- Make sure toRevert[j] does not depend on toRevert[i] for j > i
       toRevert.size.forM fun i => do
         let fvar := toRevert[i]
-        let decl := lctx.getFVar! fvar
         i.forM fun j => do
           let prevFVar := toRevert[j]
           let prevDecl := lctx.getFVar! prevFVar
diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index 68f87d6d57..8dce703daa 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -102,7 +102,7 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.const n                             => getConstAlias formatterAliasesRef n
   | ParserDescr.unary n d                           => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d)
   | ParserDescr.binary n d₁ d₂                      => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
-  | ParserDescr.node k prec d                       => return node.formatter k (← interpretParserDescr d)
+  | ParserDescr.node k _ d                          => return node.formatter k (← interpretParserDescr d)
   | ParserDescr.nodeWithAntiquot _ k d              => return node.formatter k (← interpretParserDescr d)
   | ParserDescr.sepBy p sep psep trail              => return sepBy.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.sepBy1 p sep psep trail             => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index adfef67178..34db350bec 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -276,7 +276,7 @@ end ParserState
 def ParserFn := ParserContext → ParserState → ParserState
 
 instance : Inhabited ParserFn where
-  default := fun ctx s => s
+  default := fun _ s => s
 
 inductive FirstTokens where
   | epsilon   : FirstTokens
@@ -748,7 +748,6 @@ partial def whitespace : ParserFn := fun c s =>
       if curr == '-' then andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next input i)
       else s
     else if curr == '/' then
-      let startPos := i
       let i        := input.next i
       let curr     := input.get i
       if curr == '-' then
@@ -1487,25 +1486,23 @@ def anyOfFn : List Parser → ParserFn
   { fn := checkLineEqFn errorMsg }
 
 @[inline] def withPosition (p : Parser) : Parser := {
-  info := p.info,
+  info := p.info
   fn   := fun c s =>
     p.fn { c with savedPos? := s.pos } s
 }
 
 @[inline] def withoutPosition (p : Parser) : Parser := {
-  info := p.info,
-  fn   := fun c s =>
-    let pos := c.fileMap.toPosition s.pos
-    p.fn { c with savedPos? := none } s
+  info := p.info
+  fn   := fun c s => p.fn { c with savedPos? := none } s
 }
 
 @[inline] def withForbidden (tk : Token) (p : Parser) : Parser := {
-  info := p.info,
+  info := p.info
   fn   := fun c s => p.fn { c with forbiddenTk? := tk } s
 }
 
 @[inline] def withoutForbidden (p : Parser) : Parser := {
-  info := p.info,
+  info := p.info
   fn   := fun c s => p.fn { c with forbiddenTk? := none } s
 }
 
@@ -1863,8 +1860,6 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) (s :
   It should not be added to the regular leading parsers because it would heavily
   overlap with antiquotation parsers nested inside them. -/
 @[inline] def prattParser (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) (antiquotParser : ParserFn) : ParserFn := fun c s =>
-  let iniSz  := s.stackSize
-  let iniPos := s.pos
   let s := leadingParser kind tables behavior antiquotParser c s
   if s.hasError then
     s
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index d99075acf4..c5d0e28a6e 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -102,7 +102,7 @@ def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
 abbrev getCategory (categories : ParserCategories) (catName : Name) : Option ParserCategory :=
   categories.find? catName
 
-def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories :=
+def addLeadingParser (categories : ParserCategories) (catName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories :=
   match getCategory categories catName with
   | none     =>
     throwUnknownParserCategory catName
@@ -132,9 +132,9 @@ def addTrailingParser (categories : ParserCategories) (catName : Name) (p : Trai
   | none     => throwUnknownParserCategory catName
   | some cat => pure $ categories.insert catName { cat with tables := addTrailingParserAux cat.tables p prio }
 
-def addParser (categories : ParserCategories) (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories :=
+def addParser (categories : ParserCategories) (catName : Name) (_declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories :=
   match leading, p with
-  | true, p  => addLeadingParser categories catName declName p prio
+  | true, p  => addLeadingParser categories catName p prio
   | false, p => addTrailingParser categories catName p prio
 
 def addParserTokens (tokenTable : TokenTable) (info : ParserInfo) : Except String TokenTable :=
@@ -293,7 +293,7 @@ builtin_initialize
   registerBuiltinAttribute {
     name  := `runBuiltinParserAttributeHooks,
     descr := "explicitly run hooks normally activated by builtin parser attributes",
-    add   := fun decl stx persistent => do
+    add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       runParserAttributeHooks Name.anonymous decl (builtin := true)
   }
@@ -302,7 +302,7 @@ builtin_initialize
   registerBuiltinAttribute {
     name  := `runParserAttributeHooks,
     descr := "explicitly run hooks normally activated by parser attributes",
-    add   := fun decl stx persistent => do
+    add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       runParserAttributeHooks Name.anonymous decl (builtin := false)
   }
@@ -341,8 +341,8 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
 unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
   let categories := (parserExtension.getState ctx.env).categories
   match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
-  | Except.ok (bool, p) => return p.fn ctx s
-  | Except.error e => return s.mkUnexpectedError e.toString
+  | .ok (_, p) => return p.fn ctx s
+  | .error e   => return s.mkUnexpectedError e.toString
 
 @[implementedBy evalParserConstUnsafe]
 constant evalParserConst (declName : Name) : ParserFn
@@ -467,7 +467,6 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   let prio ← Attribute.Builtin.getPrio stx
   unless kind == AttributeKind.global do throwError "invalid attribute '{attrName}', must be global"
   let decl ← getConstInfo declName
-  let env ← getEnv
   match decl.type with
   | Expr.const `Lean.Parser.TrailingParser _ _ =>
     declareTrailingBuiltinParser catName declName prio
@@ -492,10 +491,9 @@ def registerBuiltinParserAttribute (attrName : Name) (catName : Name) (behavior
    applicationTime := AttributeApplicationTime.afterCompilation
   }
 
-private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+private def ParserAttribute.add (_attrName : Name) (catName : Name) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
   let prio ← Attribute.Builtin.getPrio stx
   let env ← getEnv
-  let opts ← getOptions
   let categories := (parserExtension.getState env).categories
   let p ← mkParserOfConstant categories declName
   let leading    := p.1
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 1400d8aa56..64d126467c 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -38,7 +38,7 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
     try pure <| some (← reduceEval e) catch _ => pure none
   let e ← whnfCore e
   if e matches Expr.lam .. then
-    lambdaLetTelescope e fun xs e => parserNodeKind? e
+    lambdaLetTelescope e fun _ e => parserNodeKind? e
   else if e.isAppOfArity ``nodeWithAntiquot 4 then
     reduceEval? (e.getArg! 1)
   else if e.isAppOfArity ``withAntiquot 2 then
@@ -63,7 +63,6 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
   | _ => do
     let fn := e.getAppFn
     let .const c .. := fn | throwError "call of unknown parser at '{e}'"
-    let args := e.getAppArgs
     -- call the translated `p` with (a prefix of) the arguments of `e`, recursing for arguments
     -- of type `ty` (i.e. formerly `Parser`)
     let mkCall (p : Name) := do
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 28d3f928c8..6bcd336b6c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -241,7 +241,7 @@ partial def delab : Delab := do
   let e ← getExpr
 
   -- no need to hide atomic proofs
-  if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => pure false) then
+  if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch _ => pure false) then
     if ← getPPOption getPPProofsWithType then
       let stx ← withType delab
       return ← ``((_ : $stx))
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 52fdaa50ba..0b0f71c43c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -87,7 +87,6 @@ where
 -- NOTE: not a registered delaborator, as `const` is never called (see [delab] description)
 def delabConst : Delab := do
   let Expr.const c₀ ls _ ← getExpr | unreachable!
-  let ctx ← read
   let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
 
   let mut c ← unresolveNameGlobal c₀
@@ -212,9 +211,9 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
 def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
   if not (isCoe (← getExpr)) then failure
   match stx with
-  | `($fn $arg)   => return arg
-  | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
-  | _             => failure
+  | `($_ $arg)   => return arg
+  | `($_ $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
+  | _            => failure
 
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv
@@ -520,7 +519,6 @@ def delabLam : Delab :=
     let e ← getExpr
     let stxT ← withBindingDomain delab
     let ppTypes ← getPPOption getPPFunBinderTypes
-    let expl ← getPPOption getPPExplicit
     let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
 
     -- leave lambda implicit if possible
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 8fb7a72ff3..38423a798b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -135,7 +135,7 @@ def getPPAnalysisBlockImplicit   (o : Options) : Bool := o.get `pp.analysis.bloc
 namespace PrettyPrinter.Delaborator
 
 def returnsPi (motive : Expr) : MetaM Bool := do
-  lambdaTelescope motive fun xs b => return b.isForall
+  lambdaTelescope motive fun _ b => return b.isForall
 
 def isNonConstFun (motive : Expr) : MetaM Bool := do
   match motive with
@@ -278,7 +278,7 @@ def tryUnify (e₁ e₂ : Expr) : AnalyzeM Unit := do
     let r ← isDefEqAssigning e₁ e₂
     if !r then modify fun s => { s with postponed := s.postponed.push (e₁, e₂) }
     pure ()
-  catch ex =>
+  catch _ =>
     modify fun s => { s with postponed := s.postponed.push (e₁, e₂) }
 
 partial def inspectOutParams (arg mvar : Expr) : AnalyzeM Unit := do
@@ -372,7 +372,7 @@ mutual
     trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}"
     let e ← getExpr
     let opts ← getOptions
-    if ← (pure !e.isAtomic) <&&> pure !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => pure false) then
+    if ← (pure !e.isAtomic) <&&> pure !(getPPProofs opts) <&&> (try Meta.isProof e catch _ => pure false) then
       if getPPProofsWithType opts then
         withType $ withKnowing true true $ analyze
       return ()
@@ -515,7 +515,7 @@ mutual
         modify fun s => { s with higherOrders := s.higherOrders.set! i true }
 
     hBinOpHeuristic := do
-      let { args, mvars, bInfos, ..} ← read
+      let { mvars, ..} ← read
       if ← (pure (isHBinOp (← getExpr)) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
         tryUnify mvars[0] mvars[1]
 
@@ -610,7 +610,7 @@ mutual
           tryUnify mvars[i] args[i]
 
     maybeSetExplicit := do
-      let { f, args, mvars, bInfos, forceRegularApp, ..} ← read
+      let { f, args, bInfos, ..} ← read
       if (← get).namedArgs.any nameNotRoundtrippable then
         annotateBool `pp.explicit
         for i in [:args.size] do
@@ -634,7 +634,7 @@ def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
         let knowsType := getPPAnalyzeKnowsType (← getOptions)
         ϕ { knowsType := knowsType, knowsLevel := knowsType, subExpr := mkRoot e }
           |>.run' { : TopDownAnalyze.State }
-      catch ex =>
+      catch _ =>
         trace[pp.analyze.error] "failed"
         pure {}
       finally set s₀
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 4a1514a69c..4871e67ce3 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -260,15 +260,15 @@ def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
   categoryParser.formatter stx.getId
 
 @[combinatorFormatter Lean.Parser.parserOfStack]
-def parserOfStack.formatter (offset : Nat) (prec : Nat := 0) : Formatter := do
+def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do
   let st ← get
   let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
   formatterForKind stx.getKind
 
 @[combinatorFormatter Lean.Parser.error]
-def error.formatter (msg : String) : Formatter := pure ()
+def error.formatter (_msg : String) : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.errorAtSavedPos]
-def errorAtSavedPos.formatter (msg : String) (delta : Bool) : Formatter := pure ()
+def errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.atomic]
 def atomic.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.lookahead]
@@ -405,7 +405,7 @@ def identNoAntiquot.formatter : Formatter := do
   pushToken info id.toString
   goLeft
 
-@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter (id : Name) := rawIdentNoAntiquot.formatter
+@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
 
 def visitAtom (k : SyntaxNodeKind) : Formatter := do
   let stx ← getCur
@@ -450,16 +450,16 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 
 @[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p
-@[combinatorFormatter Lean.Parser.withForbidden] def withForbidden.formatter (tk : Token) (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.withoutInfo] def withoutInfo.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.setExpected]
-def setExpected.formatter (expected : List String) (p : Formatter) : Formatter := p
+def setExpected.formatter (_expected : List String) (p : Formatter) : Formatter := p
 
 @[combinatorFormatter Lean.Parser.incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
-@[combinatorFormatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (declName : Name) (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (_declName : Name) (p : Formatter) : Formatter := p
 
 @[combinatorFormatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
   let st ← get
@@ -495,7 +495,7 @@ def interpolatedStr.formatter (p : Formatter) : Formatter := do
     | some str => push str *> goLeft
     | none     => p
 
-@[combinatorFormatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (label : String) (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (_label : String) (p : Formatter) : Formatter := p
 
 @[combinatorFormatter ite, macroInline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Formatter) : Formatter :=
   if c then t else e
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 38e732a2f4..6f230e849a 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -129,7 +129,7 @@ unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
   } `Lean.PrettyPrinter.parenthesizerAttribute
 @[builtinInit mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer
 
-abbrev CategoryParenthesizer := forall (prec : Nat), Parenthesizer
+abbrev CategoryParenthesizer := (prec : Nat) → Parenthesizer
 
 unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryParenthesizer) :=
   KeyedDeclsAttribute.init {
@@ -249,7 +249,6 @@ def visitToken : Parenthesizer := do
   goLeft
 
 @[combinatorParenthesizer Lean.Parser.orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
-  let st ← get
   -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
   -- them in turn. Uses the syntax traverser non-linearly!
   p1 <|> p2
@@ -301,7 +300,7 @@ def tokenWithAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
   else
     p
 
-def parenthesizeCategoryCore (cat : Name) (prec : Nat) : Parenthesizer :=
+def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer :=
   withReader (fun ctx => { ctx with cat := cat }) do
     let stx ← getCur
     if stx.getKind == `choice then
@@ -328,14 +327,13 @@ def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesi
   categoryParser.parenthesizer stx.getId prec
 
 @[combinatorParenthesizer Lean.Parser.parserOfStack]
-def parserOfStack.parenthesizer (offset : Nat) (prec : Nat := 0) : Parenthesizer := do
+def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesizer := do
   let st ← get
   let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
   parenthesizerForKind stx.getKind
 
 @[builtinCategoryParenthesizer term]
 def term.parenthesizer : CategoryParenthesizer | prec => do
-  let stx ← getCur
   maybeParenthesize `term true (fun stx => Unhygienic.run `(($stx))) prec $
     parenthesizeCategoryCore `term prec
 
@@ -354,11 +352,11 @@ def rawStx.parenthesizer : CategoryParenthesizer | _ => do
   goLeft
 
 @[combinatorParenthesizer Lean.Parser.error]
-def error.parenthesizer (msg : String) : Parenthesizer :=
+def error.parenthesizer (_msg : String) : Parenthesizer :=
   pure ()
 
 @[combinatorParenthesizer Lean.Parser.errorAtSavedPos]
-def errorAtSavedPos.parenthesizer (msg : String) (delta : Bool) : Parenthesizer :=
+def errorAtSavedPos.parenthesizer (_msg : String) (_delta : Bool) : Parenthesizer :=
   pure ()
 
 @[combinatorParenthesizer Lean.Parser.atomic]
@@ -417,15 +415,15 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Pa
     -- parser is calling us.
     categoryParser.parenthesizer ctx.cat lhsPrec
 
-@[combinatorParenthesizer Lean.Parser.rawCh] def rawCh.parenthesizer (ch : Char) := visitToken
+@[combinatorParenthesizer Lean.Parser.rawCh] def rawCh.parenthesizer (_ch : Char) := visitToken
 
-@[combinatorParenthesizer Lean.Parser.symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (sym : String) := visitToken
-@[combinatorParenthesizer Lean.Parser.unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (sym asciiSym : String) := visitToken
+@[combinatorParenthesizer Lean.Parser.symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (_sym : String) := visitToken
+@[combinatorParenthesizer Lean.Parser.unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken
 
 @[combinatorParenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken
-@[combinatorParenthesizer Lean.Parser.identEq] def identEq.parenthesizer (id : Name) := visitToken
-@[combinatorParenthesizer Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (sym : String) (includeIdent : Bool) := visitToken
+@[combinatorParenthesizer Lean.Parser.identEq] def identEq.parenthesizer (_id : Name) := visitToken
+@[combinatorParenthesizer Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken
 
 @[combinatorParenthesizer Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken
@@ -467,16 +465,16 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
   modify fun st => { st with contPrec := none }
   p
 @[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
-@[combinatorParenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.withoutInfo] def withoutInfo.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.setExpected]
-def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer := p
+def setExpected.parenthesizer (_expected : List String) (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer Lean.Parser.incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
-@[combinatorParenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (declName : Name) (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (_declName : Name) (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
@@ -503,7 +501,7 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
     else
       p
 
-@[combinatorParenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (label : String) (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (_label : String) (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer ite, macroInline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Parenthesizer) : Parenthesizer :=
   if c then t else e
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 09da7a3509..832e2fc8af 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -55,7 +55,7 @@ private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM
       unless hasMVarHead do
         let targetTypeNumArgs ← getExpectedNumArgs expectedType
         numArgs := numArgs - targetTypeNumArgs
-      let (newMVars, _, type) ← forallMetaTelescopeReducing type (some numArgs)
+      let (_, _, type) ← forallMetaTelescopeReducing type (some numArgs)
       -- TODO take coercions into account
       -- We use `withReducible` to make sure we don't spend too much time unfolding definitions
       -- Alternative: use default and small number of heartbeats
@@ -406,7 +406,7 @@ private def tacticCompletion (ctx : ContextInfo) : IO (Option CompletionList) :=
   -- Just return the list of tactics for now.
   ctx.runMetaM {} do
     let table := Parser.getCategory (Parser.parserExtension.getState (← getEnv)).categories `tactic |>.get!.tables.leadingTable
-    let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk parser =>
+    let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk _ =>
       -- TODO pretty print tactic syntax
       items.push ({ label := tk.toString, detail? := none, documentation? := none, kind? := CompletionItemKind.keyword }, 1)
     return some { items := sortCompletionItems items, isIncomplete := true }
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 092c259914..505c189fc1 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -127,7 +127,6 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
 open Elab GoToKind in
 def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
     : RequestM (RequestTask (Array LocationLink)) := do
-  let rc ← read
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
@@ -204,7 +203,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
   let pos := text.lspPosToUtf8Pos p.position
 
   let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
-    | stx@`(doElem|return%$i $e) => Id.run do
+    | `(doElem|return%$i $e) => Id.run do
       if let some range := i.getRange? then
         if range.contains pos then
           return some { range := doRange?.getD (range.toLspRange text), kind? := DocumentHighlightKind.text }
@@ -212,7 +211,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
     | `(do%$i $elems) => highlightReturn? (i.getRange?.get!.toLspRange text) elems
     | stx => stx.getArgs.findSome? (highlightReturn? doRange?)
 
-  let highlightRefs? (snaps : Array Snapshot) (pos : Lsp.Position) : Option (Array DocumentHighlight) := Id.run do
+  let highlightRefs? (snaps : Array Snapshot) : Option (Array DocumentHighlight) := Id.run do
     let trees := snaps.map (·.infoTree)
     let refs : Lsp.ModuleRefs := findModuleRefs text trees
     let mut ranges := #[]
@@ -228,7 +227,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
   withWaitFindSnap doc (fun s => s.endPos > pos)
     (notFoundX := pure #[]) fun snap => do
       let (snaps, _) ← doc.allSnaps.updateFinishedPrefix
-      if let some his := highlightRefs? snaps.finishedPrefix.toArray p.position then
+      if let some his := highlightRefs? snaps.finishedPrefix.toArray then
         return his
       if let some hi := highlightReturn? none snap.stx then
         return #[hi]
@@ -258,14 +257,14 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams)
     | stx::stxs => match stx with
       | `(namespace $id)  => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id
       | `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.getD stx)
-      | `(end $(id)?) => ([], stx::stxs)
+      | `(end $(_id)?) => ([], stx::stxs)
       | _ => Id.run do
         let (syms, stxs') := toDocumentSymbols text stxs
         unless stx.isOfKind ``Lean.Parser.Command.declaration do
           return (syms, stxs')
         if let some stxRange := stx.getRange? then
           let (name, selection) := match stx with
-            | `($dm:declModifiers $ak:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $val) =>
+            | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $_) =>
               ((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig)
             | _ => match stx[1][1] with
               | `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id)
@@ -367,7 +366,7 @@ where
           addToken ti.stx SemanticTokenType.property
           lastPos := ti.stx.getPos?.get!
   highlightKeyword stx := do
-    if let Syntax.atom info val := stx then
+    if let Syntax.atom _ val := stx then
       if (val.length > 0 && val[0].isAlpha) ||
          -- Support for keywords of the form `#<alpha>...`
          (val.length > 1 && val[0] == '#' && val[⟨1⟩].isAlpha) then
@@ -414,9 +413,9 @@ partial def handleFoldingRange (_ : FoldingRangeParams)
     addRanges (text : FileMap) sections
     | [] => return
     | stx::stxs => match stx with
-      | `(namespace $id)  => addRanges text (stx.getPos?::sections) stxs
-      | `(section $(id)?) => addRanges text (stx.getPos?::sections) stxs
-      | `(end $(id)?) => do
+      | `(namespace $_id)  => addRanges text (stx.getPos?::sections) stxs
+      | `(section $(_id)?) => addRanges text (stx.getPos?::sections) stxs
+      | `(end $(_id)?) => do
         if let start::rest := sections then
           addRange text FoldingRangeKind.region start stx.getTailPos?
           addRanges text rest stxs
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index edc87ccb88..de1df17521 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -198,7 +198,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
       trace[Elab.Deriving.RpcEncoding] m!"RpcEncoding type binders : {ts}"
 
       let packetNm ← mkFreshUserName `RpcEncodingPacket
-      let st ← foldWithConstructors indVal params (init := st) fun acc ctor argVars tp => do
+      let st ← foldWithConstructors indVal params (init := st) fun acc ctor argVars _ => do
         -- create the constructor
         let mut pktCtorTp := Lean.mkConst packetNm
         for arg in argVars.reverse do
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 0c237e4d6a..538384c7cd 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -128,7 +128,7 @@ builtin_initialize registerBuiltinAttribute {
     The function must have type `α → RequestM (RequestTask β)` with
     RpcEncodings for both α and β."
   applicationTime := AttributeApplicationTime.afterCompilation
-  add := fun decl stx kind =>
+  add := fun decl _ _ =>
     registerRpcProcedure decl
 }
 
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 86589b09f0..79f16b8630 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -74,7 +74,7 @@ def isAtEnd (s : Snapshot) : Bool :=
 end Snapshot
 
 /-- Reparses the header syntax but does not re-elaborate it. Used to ignore whitespace-only changes. -/
-def reparseHeader (inputCtx : Parser.InputContext) (header : Snapshot) (opts : Options := {}) : IO Snapshot := do
+def reparseHeader (inputCtx : Parser.InputContext) (header : Snapshot) : IO Snapshot := do
   let (newStx, newMpState, _) ← Parser.parseHeader inputCtx
   pure { header with stx := newStx, mpState := newMpState }
 
@@ -149,7 +149,7 @@ def compileNextCmd (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidget
         (getResetInfoTrees *> Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post
-    snap.tacticCache.modify fun { pre, post } => { pre := postNew, post := {} }
+    snap.tacticCache.modify fun _ => { pre := postNew, post := {} }
     let mut postCmdState ← cmdStateRef.get
     if !output.isEmpty then
       postCmdState := {
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index c46d06fa98..92626ca01d 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -408,7 +408,7 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf
   return symbols
     |>.qsort (fun ((_, s1), _) ((_, s2), _) => s1 > s2)
     |>.extract 0 100 -- max amount
-    |>.map fun ((name, score), location) =>
+    |>.map fun ((name, _), location) =>
       { name, kind := SymbolKind.constant, location }
 
 end RequestHandling
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 3fff080c94..1a5adf2720 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -193,7 +193,7 @@ def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structN
 /-- Return true iff `constName` is the a non-recursive inductive datatype that has only one constructor. -/
 def isStructureLike (env : Environment) (constName : Name) : Bool :=
   match env.find? constName with
-  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) => true
+  | some (ConstantInfo.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
   | _ => false
 
 /-- Return number of fields for a structure-like type -/
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 158713d370..7da4042f97 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -127,12 +127,12 @@ trail.startPos + trail.posOf '\n'
    or the beginning of the String. -/
 @[inline]
 private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
-  | atom info@(SourceInfo.original lead _ trail _) val => do
+  | atom info@(SourceInfo.original _ _ trail _) val => do
     let trailStop := chooseNiceTrailStop trail
     let newInfo := updateInfo info (← get) trailStop
     set trailStop
     return some (atom newInfo val)
-  | ident info@(SourceInfo.original lead _ trail _) rawVal val pre => do
+  | ident info@(SourceInfo.original _ _ trail _) rawVal val pre => do
     let trailStop := chooseNiceTrailStop trail
     let newInfo := updateInfo info (← get) trailStop
     set trailStop
@@ -173,8 +173,8 @@ partial def getTailWithPos : Syntax → Option Syntax
   | stx@(atom info _)   => info.getPos?.map fun _ => stx
   | stx@(ident info ..) => info.getPos?.map fun _ => stx
   | node SourceInfo.none _ args => args.findSomeRev? getTailWithPos
-  | stx@(node info _ _) => stx
-  | _                   => none
+  | stx@(node ..) => stx
+  | _ => none
 
 open SourceInfo in
 /-- Split an `ident` into its dot-separated components while preserving source info.
@@ -423,8 +423,8 @@ def antiquotKind? : Syntax → Option SyntaxNodeKind
 
 -- An "antiquotation splice" is something like `$[...]?` or `$[...]*`.
 def antiquotSpliceKind? : Syntax → Option SyntaxNodeKind
-  | Syntax.node _ (Name.str k "antiquot_scope" _) args => some k
-  | _                                                  => none
+  | Syntax.node _ (Name.str k "antiquot_scope" _) _ => some k
+  | _ => none
 
 def isAntiquotSplice (stx : Syntax) : Bool :=
   antiquotSpliceKind? stx |>.isSome
@@ -445,8 +445,8 @@ def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suff
 
 -- `$x,*` etc.
 def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
-  | Syntax.node _ (Name.str k "antiquot_suffix_splice" _) args => some k
-  | _                                                          => none
+  | Syntax.node _ (Name.str k "antiquot_suffix_splice" _) _ => some k
+  | _ => none
 
 def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
   antiquotSuffixSplice? stx |>.isSome
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index eff4126e78..d0da100104 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -46,9 +46,9 @@ structure PPFns where
 
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
-    ppExpr := fun ctx e      => return format (toString e),
-    ppTerm := fun ctx stx    => return stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
-    ppGoal := fun ctx mvarId => return "goal"
+    ppExpr := fun _ e => return format (toString e)
+    ppTerm := fun ctx stx => return stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
+    ppGoal := fun _ _ => return "goal"
   }
 
 builtin_initialize ppExt : EnvExtension PPFns ←
diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean
index 40ad8880fa..ddb3cda569 100644
--- a/src/Lean/Widget/TaggedText.lean
+++ b/src/Lean/Widget/TaggedText.lean
@@ -75,7 +75,7 @@ private structure TaggedState where
 
 instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where
   pushOutput s       := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩
-  pushNewline indent := modify fun ⟨out, ts, col⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩
+  pushNewline indent := modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩
   currColumn         := return (←get).column
   startTag n         := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩
   endTags n          := modify fun ⟨out, ts, col⟩ =>
diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean
index a586c3e14b..e19d044060 100644
--- a/src/Std/Data/PersistentArray.lean
+++ b/src/Std/Data/PersistentArray.lean
@@ -212,6 +212,7 @@ variable {β : Type v}
 @[specialize] def foldrM [Monad m] (t : PersistentArray α) (f : α → β → m β) (init : β) : m β := do
   foldrMAux f t.root (← t.tail.foldrM f init)
 
+set_option linter.unusedVariables.funArgs false in
 @[specialize]
 partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β]
     (f : α → β → m (ForInStep β)) (n : PersistentArrayNode α) (b : β) : m (ForInStep β) := do
diff --git a/tests/lean/simpZetaFalse.lean.expected.out b/tests/lean/simpZetaFalse.lean.expected.out
index 1d3b02710f..b532343f64 100644
--- a/tests/lean/simpZetaFalse.lean.expected.out
+++ b/tests/lean/simpZetaFalse.lean.expected.out
@@ -10,11 +10,13 @@ theorem ex1 : ∀ (x : Nat),
       1 :=
 fun x h =>
   Eq.mpr
-    (congrFun
-      (congrArg Eq
-        (let_congr (Eq.refl (x * x)) fun y =>
-          ite_congr (Eq.trans (congrFun (congrArg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a => Eq.refl (y + 1)))
-      1)
+    (id
+      (congrFun
+        (congrArg Eq
+          (let_congr (Eq.refl (x * x)) fun y =>
+            ite_congr (Eq.trans (congrFun (congrArg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a =>
+              Eq.refl (y + 1)))
+        1))
     (of_eq_true (eq_self 1))
 x z : Nat
 h : f (f x) = x
@@ -29,7 +31,7 @@ theorem ex2 : ∀ (x z : Nat),
         y) =
         z :=
 fun x z h h' =>
-  Eq.mpr (congrFun (congrArg Eq (let_val_congr (fun y => y) h)) z)
+  Eq.mpr (id (congrFun (congrArg Eq (let_val_congr (fun y => y) h)) z))
     (of_eq_true (Eq.trans (congrArg (Eq x) h') (eq_self x)))
 x z : Nat
 ⊢ (let α := Nat;
@@ -46,5 +48,5 @@ theorem ex4 : ∀ (p : Prop),
       fun x => x = x) =
       fun z => p :=
 fun p h =>
-  Eq.mpr (congrFun (congrArg Eq (let_body_congr 10 fun n => funext fun x => eq_self x)) fun z => p)
+  Eq.mpr (id (congrFun (congrArg Eq (let_body_congr 10 fun n => funext fun x => eq_self x)) fun z => p))
     (of_eq_true (Eq.trans (congrArg (Eq fun x => True) (funext fun z => eq_true h)) (eq_self fun x => True)))
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index fdf3093dcf..38c47c9012 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
-    2 * a (n - 1) (_ : Nat.pred n < n)
+    2 * a (n - 1) (_ : (measure id).1 (n - 1) n)