diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index c4814d4682..b5297ee7ae 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -56,7 +56,7 @@ theorem em (p : Prop) : p ∨ ¬p :=
   | Or.inl hne => Or.inr (mt p_implies_uv hne)
   | Or.inr h   => Or.inl h
 
-theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ x : α, True
+theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
   | ⟨x⟩ => ⟨x, trivial⟩
 
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
@@ -75,7 +75,7 @@ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 
 noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
-  fun x y => inferInstance
+  fun _ _ => inferInstance
 
 noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
   match (propDecidable (Nonempty α)) with
diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 286b3947c8..91e57bb8ed 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -27,11 +27,11 @@ class CoeTail (α : Sort u) (β : Sort v) where
 class CoeHTCT (α : Sort u) (β : Sort v) where
   coe : α → β
 
-class CoeDep (α : Sort u) (a : α) (β : Sort v) where
+class CoeDep (α : Sort u) (_ : α) (β : Sort v) where
   coe : β
 
 /- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
-class CoeT (α : Sort u) (a : α) (β : Sort v) where
+class CoeT (α : Sort u) (_ : α) (β : Sort v) where
   coe : β
 
 class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 1cf68d58dc..130c2575da 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -50,7 +50,7 @@ variable {ε : Type u}
 def orElseLazy (x : Except ε α) (y : Unit → Except ε α) : Except ε α :=
   match x with
   | Except.ok a    => Except.ok a
-  | Except.error e => y ()
+  | Except.error _ => y ()
 
 instance : Monad (Except ε) where
   pure := Except.pure
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 7372222f2b..55d88ec54f 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -16,7 +16,7 @@ namespace ReaderT
   fun s => x₁ s <|> x₂ () s
 
 @[inline] protected def failure [Alternative m] : ReaderT ρ m α :=
-  fun s => failure
+  fun _ => failure
 
 instance [Alternative m] [Monad m] : Alternative (ReaderT ρ m) where
   failure := ReaderT.failure
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index cc65ad3d36..cda996a0f9 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -53,7 +53,7 @@ instance : Monad (StateT σ m) where
   fun s => x₁ s <|> x₂ () s
 
 @[inline] protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
-  fun s => failure
+  fun _ => failure
 
 instance [Alternative m] : Alternative (StateT σ m) where
   failure := StateT.failure
@@ -63,7 +63,7 @@ instance [Alternative m] : Alternative (StateT σ m) where
   fun s => pure (s, s)
 
 @[inline] protected def set : σ → StateT σ m PUnit :=
-  fun s' s => pure (⟨⟩, s')
+  fun s' _ => pure (⟨⟩, s')
 
 @[inline] protected def modifyGet (f : σ → α × σ) : StateT σ m α :=
   fun s => pure (f s)
diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean
index 6a1c39c835..ca5f9e50f9 100644
--- a/src/Init/Control/StateCps.lean
+++ b/src/Init/Control/StateCps.lean
@@ -21,19 +21,19 @@ namespace StateCpsT
   runK x s (fun a s => pure (a, s))
 
 @[inline] def run' {α σ : Type u} {m : Type u → Type v}  [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
-  runK x s (fun a s => pure a)
+  runK x s (fun a _ => pure a)
 
 instance : Monad (StateCpsT σ m) where
   map  f x := fun δ s k => x δ s fun a s => k (f a) s
-  pure a   := fun δ s k => k a s
+  pure a   := fun _ s k => k a s
   bind x f := fun δ s k => x δ s fun a s => f a δ s k
 
 instance : LawfulMonad (StateCpsT σ m) := by
   refine' { .. } <;> intros <;> rfl
 
 instance : MonadStateOf σ (StateCpsT σ m) where
-  get   := fun δ s k => k s s
-  set s := fun δ _ k => k ⟨⟩ s
+  get   := fun _ s k => k s s
+  set s := fun _ _ k => k ⟨⟩ s
   modifyGet f := fun _ s k => let (a, s) := f s; k a s
 
 @[inline] protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
@@ -68,6 +68,6 @@ instance [Monad m] : MonadLift m (StateCpsT σ m) where
 
 @[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl
 
-@[simp] theorem run'_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run' s = x.runK s (fun a s => pure a) := rfl
+@[simp] theorem run'_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run' s = x.runK s (fun a _ => pure a) := rfl
 
 end StateCpsT
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 7dde9d3919..59ba59f207 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -89,7 +89,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
 
 export ForIn (forIn)
 
-class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam $ Membership α ρ) where
+class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (_ : outParam $ Membership α ρ) where
   forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')
@@ -273,10 +273,10 @@ end Ne
 
 theorem Bool.of_not_eq_true : {b : Bool} → ¬ (b = true) → b = false
   | true,  h => absurd rfl h
-  | false, h => rfl
+  | false, _ => rfl
 
 theorem Bool.of_not_eq_false : {b : Bool} → ¬ (b = false) → b = true
-  | true,  h => rfl
+  | true,  _ => rfl
   | false, h => absurd rfl h
 
 theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b := by
@@ -366,12 +366,12 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 theorem decide_true_eq_true (h : Decidable True) : @decide True h = true :=
   match h with
-  | isTrue h  => rfl
+  | isTrue _  => rfl
   | isFalse h => False.elim <| h ⟨⟩
 
 theorem decide_false_eq_false (h : Decidable False) : @decide False h = false :=
   match h with
-  | isFalse h => rfl
+  | isFalse _ => rfl
   | isTrue h  => False.elim h
 
 /-- Similar to `decide`, but uses an explicit instance -/
@@ -436,7 +436,7 @@ end
 
 @[macroInline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) :=
   if hp : p then
-    if hq : q then isTrue (fun h => hq)
+    if hq : q then isTrue (fun _ => hq)
     else isFalse (fun h => absurd (h hp) hq)
   else isTrue (fun h => absurd h hp)
 
@@ -456,34 +456,34 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
 
 theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
   match h with
-  | isTrue  hc  => rfl
+  | isTrue  _   => rfl
   | isFalse hnc => absurd hc hnc
 
 theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
   match h with
   | isTrue hc   => absurd hc hnc
-  | isFalse hnc => rfl
+  | isFalse _   => rfl
 
 theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
   match h with
-  | isTrue  hc  => rfl
+  | isTrue  _   => rfl
   | isFalse hnc => absurd hc hnc
 
 theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
   match h with
   | isTrue hc   => absurd hc hnc
-  | isFalse hnc => rfl
+  | isFalse _   => rfl
 
 -- Remark: dite and ite are "defally equal" when we ignore the proofs.
-theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
   match h with
-  | isTrue hc   => rfl
-  | isFalse hnc => rfl
+  | isTrue _    => rfl
+  | isFalse _   => rfl
 
 instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)  :=
   match dC with
-  | isTrue hc  => dT
-  | isFalse hc => dE
+  | isTrue _   => dT
+  | isFalse _  => dE
 
 instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h)  :=
   match dC with
@@ -511,7 +511,7 @@ instance : Inhabited Prop where
 deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
 
 theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
-  | ⟨w, h⟩ => ⟨w⟩
+  | ⟨w, _⟩ => ⟨w⟩
 
 /- Subsingleton -/
 
@@ -532,11 +532,11 @@ instance (p : Prop) : Subsingleton p :=
 instance (p : Prop) : Subsingleton (Decidable p) :=
   Subsingleton.intro fun
     | isTrue t₁ => fun
-      | isTrue t₂  => rfl
+      | isTrue _   => rfl
       | isFalse f₂ => absurd t₁ f₂
     | isFalse f₁ => fun
       | isTrue t₂  => absurd t₂ f₁
-      | isFalse f₂ => rfl
+      | isFalse _  => rfl
 
 theorem recSubsingleton
      {p : Prop} [h : Decidable p]
@@ -576,7 +576,7 @@ def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (f
 variable {α : Type u} {p : α → Prop}
 
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
-  | ⟨x, h1⟩, ⟨_, _⟩, rfl => rfl
+  | ⟨_, _ ⟩, ⟨_, _⟩, rfl => rfl
 
 theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
@@ -597,10 +597,10 @@ end Subtype
 section
 variable {α : Type u} {β : Type v}
 
-instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) where
+instance Sum.inhabitedLeft [_ : Inhabited α] : Inhabited (Sum α β) where
   default := Sum.inl default
 
-instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) where
+instance Sum.inhabitedRight [_ : Inhabited β] : Inhabited (Sum α β) where
   default := Sum.inr default
 
 instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
@@ -611,8 +611,8 @@ instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Decidab
   | Sum.inr a, Sum.inr b =>
     if h : a = b then isTrue (h ▸ rfl)
     else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inl b => isFalse fun h => Sum.noConfusion h
-  | Sum.inl a, Sum.inr b => isFalse fun h => Sum.noConfusion h
+  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
+  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
 
 end
 
@@ -627,8 +627,8 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
     | isTrue e₁ =>
       match decEq b b' with
       | isTrue e₂  => isTrue (e₁ ▸ e₂ ▸ rfl)
-      | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun e₁' e₂' => absurd e₂' n₂
-    | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' e₂' => absurd e₁' n₁
+      | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun _   e₂' => absurd e₂' n₂
+    | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' _   => absurd e₁' n₁
 
 instance [BEq α] [BEq β] : BEq (α × β) where
   beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂
@@ -640,7 +640,7 @@ instance prodHasDecidableLt
     [LT α] [LT β] [DecidableEq α] [DecidableEq β]
     [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
     : (s t : α × β) → Decidable (s < t) :=
-  fun t s => inferInstanceAs (Decidable (_ ∨ _))
+  fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
 
 theorem Prod.lt_def [LT α] [LT β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
   rfl
@@ -825,7 +825,7 @@ protected abbrev hrecOn
 end
 end Quot
 
-def Quotient {α : Sort u} (s : Setoid α) :=
+def Quotient {α : Sort u} (_ : Setoid α) :=
   @Quot α Setoid.r
 
 namespace Quotient
@@ -1017,7 +1017,7 @@ variable {α : Sort u} {β : α → Sort v}
 protected def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x
 
 protected theorem Equiv.refl (f : ∀ (x : α), β x) : Function.Equiv f f :=
-  fun x => rfl
+  fun _ => rfl
 
 protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Function.Equiv f₁ f₂ → Function.Equiv f₂ f₁ :=
   fun h x => Eq.symm (h x)
@@ -1060,7 +1060,7 @@ instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsi
 
 /- Squash -/
 
-def Squash (α : Type u) := Quot (fun (a b : α) => True)
+def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
 
 def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
 
@@ -1068,7 +1068,7 @@ theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α)
   Quot.ind h
 
 @[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
-  Quot.lift f (fun a b _ => Subsingleton.elim _ _) s
+  Quot.lift f (fun _ _ _ => Subsingleton.elim _ _) s
 
 instance : Subsingleton (Squash α) where
   allEq a b := by
diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean
index 6d332944d7..b59e1a4dec 100644
--- a/src/Init/Data/AC.lean
+++ b/src/Init/Data/AC.lean
@@ -160,12 +160,12 @@ theorem Context.evalList_mergeIdem (ctx : Context α) (h : ContextInformation.is
 theorem insert_nonEmpty : insert x xs ≠ [] := by
   induction xs with
   | nil => simp [insert]
-  | cons x xs ih => simp [insert]; split <;> simp
+  | cons x xs _  => simp [insert]; split <;> simp
 
 theorem Context.sort_loop_nonEmpty (xs : List Nat) (h : xs ≠ []) : sort.loop xs ys ≠ [] := by
   induction ys generalizing xs with
   | nil => simp [sort.loop]; assumption
-  | cons y ys ih => simp [sort.loop]; apply ih; apply insert_nonEmpty
+  | cons y _  ih => simp [sort.loop]; apply ih; apply insert_nonEmpty
 
 theorem Context.evalList_insert
   (ctx : Context α)
@@ -197,7 +197,7 @@ theorem Context.evalList_sort_congr
   : evalList α ctx (sort.loop a c) = evalList α ctx (sort.loop b c) := by
   induction c generalizing a b with
   | nil => simp [sort.loop, h₂]
-  | cons c cs ih =>
+  | cons c _  ih =>
     simp [sort.loop]; apply ih; simp [evalList_insert ctx h, evalList]
     cases a with
     | nil => apply absurd h₃; simp
@@ -214,7 +214,7 @@ theorem Context.evalList_sort_loop_swap
   : evalList α ctx (sort.loop xs (y::ys)) = evalList α ctx (sort.loop (y::xs) ys) := by
   induction ys generalizing y xs with
   | nil => simp [sort.loop, evalList_insert ctx h]
-  | cons z zs ih =>
+  | cons z zs _  =>
     simp [sort.loop]; apply evalList_sort_congr ctx h
     simp [evalList_insert ctx h]
     cases h₂ : insert y xs
@@ -260,7 +260,7 @@ theorem Context.evalList_sort (ctx : Context α) (h : ContextInformation.isComm
 theorem Context.toList_nonEmpty (e : Expr) : e.toList ≠ [] := by
   induction e with
   | var => simp [Expr.toList]
-  | op l r ih₁ ih₂ =>
+  | op l r ih₁ _   =>
     simp [Expr.toList]
     cases h : l.toList with
     | nil => contradiction
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 1c5046336f..f32c7367af 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -347,12 +347,12 @@ def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
 @[inline]
 def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
-    | 0,   h => pure none
+    | 0,   _ => pure none
     | i+1, h => do
       have : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
       let r ← f (as.get ⟨i, this⟩)
       match r with
-      | some v => pure r
+      | some _ => pure r
       | none   =>
         have : i ≤ as.size := Nat.le_of_lt this
         find i this
@@ -469,7 +469,7 @@ def toList (as : Array α) : List α :=
   as.foldr List.cons []
 
 instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a n :=
+  reprPrec a _ :=
     let _ : Std.ToFormat α := ⟨repr⟩
     if a.size == 0 then
       "#[]"
@@ -706,7 +706,7 @@ def insertAt (as : Array α) (i : Nat) (a : α) : Array α :=
     as.insertAtAux i as.size
 
 def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     hi, acc => acc
+  | 0,     _,  acc => acc
   | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
 
 def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
@@ -773,7 +773,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
     false
 
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   h => true
+  | 0,   _ => true
   | i+1, h =>
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this
diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 106a73949c..918bae5688 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -31,7 +31,7 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
   | Or.inl h        =>
     apply Nat.lt_trans h
     decide
-  | Or.inr ⟨h₁, h₂⟩ =>
+  | Or.inr ⟨_,  h₂⟩ =>
     apply Nat.lt_trans h₂
     decide
 
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index ac7eff88b4..911670f6be 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -31,7 +31,7 @@ protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
 
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h
-  | a+1, h =>
+  | _+1, h =>
     have : n > 0 := Nat.lt_trans (Nat.zero_lt_succ _) h;
     Nat.mod_lt _ this
 
@@ -113,7 +113,7 @@ theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 
 theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (i % m).val < m
-  | m, ⟨a, h⟩, hp =>  Nat.lt_of_le_of_lt (mod_le _ _) (mod_lt _ hp)
+  | _, ⟨_, _⟩, hp =>  Nat.lt_of_le_of_lt (mod_le _ _) (mod_lt _ hp)
 
 end Fin
 
diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean
index 2ec8772622..2f77822676 100644
--- a/src/Init/Data/Format/Basic.lean
+++ b/src/Init/Data/Format/Basic.lean
@@ -73,9 +73,9 @@ private structure SpaceResult where
     { r₂ with space := r₁.space + r₂.space }
 
 private def spaceUptoLine : Format → Bool → Nat → SpaceResult
-  | nil,          flatten, w => {}
-  | line,         flatten, w => if flatten then { space := 1 } else { foundLine := true }
-  | text s,       flatten, w =>
+  | nil,          _,       _ => {}
+  | line,         flatten, _ => if flatten then { space := 1 } else { foundLine := true }
+  | text s,       flatten, _ =>
     let p := s.posOf '\n';
     let off := s.offsetOfPos p;
     { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
@@ -95,7 +95,7 @@ private structure WorkGroup where
   items   : List WorkItem
 
 private partial def spaceUptoLine' : List WorkGroup → Nat → SpaceResult
-  |   [],                         w => {}
+  |   [],                         _ => {}
   |   { items := [],    .. }::gs, w => spaceUptoLine' gs w
   | g@{ items := i::is, .. }::gs, w => merge w (spaceUptoLine i.f g.flatten w) (spaceUptoLine' ({ g with items := is }::gs))
 
@@ -216,8 +216,8 @@ instance : MonadPrettyFormat (StateM State) where
   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
-  startTag n         := return ()
-  endTags n          := return ()
+  startTag _         := return ()
+  endTags _          := return ()
 
 /-- Pretty-print a `Format` object as a string with expected width `w`. -/
 @[export lean_format_pretty]
@@ -240,8 +240,8 @@ instance : ToFormat String where
   format s := Format.text s
 
 def Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format
-  | [],    sep => nil
-  | [a],   sep => format a
+  | [],    _   => nil
+  | [a],   _   => format a
   | a::as, sep => format a ++ sep ++ joinSep as sep
 
 def Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format
@@ -249,7 +249,7 @@ def Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → F
   | a::as => pre ++ format a ++ prefixJoin pre as
 
 def Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format
-  | [],    suffix => nil
+  | [],    _      => nil
   | a::as, suffix => format a ++ suffix ++ joinSuffix as suffix
 
 end Std
diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean
index 2dd3ada2cf..a970c91294 100644
--- a/src/Init/Data/Format/Syntax.lean
+++ b/src/Init/Data/Format/Syntax.lean
@@ -21,7 +21,7 @@ private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Form
 
 partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Syntax → Format
   | _,     atom info val     => formatInfo showInfo info $ format (repr val)
-  | _,     ident info _ val pre => formatInfo showInfo info $ format "`" ++ format val
+  | _,     ident info _ val _   => formatInfo showInfo info $ format "`" ++ format val
   | _,     missing           => "<missing>"
   | depth, node _ kind args  =>
     let depth := depth + 1;
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index f661c8737a..3811ff7ebf 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -57,4 +57,4 @@ instance : Hashable Int where
     | Int.negSucc n => UInt64.ofNat (2 * n + 1)
 
 instance (P : Prop) : Hashable P where
-  hash p := 0
+  hash _ := 0
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 68d95ff0a1..bf538a13cf 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -107,8 +107,8 @@ protected def decEq (a b : @& Int) : Decidable (a = b) :=
   | negSucc a, negSucc b => match decEq a b with
     | isTrue h  => isTrue  <| h ▸ rfl
     | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
-  | ofNat a, negSucc b => isFalse <| fun h => Int.noConfusion h
-  | negSucc a, ofNat b => isFalse <| fun h => Int.noConfusion h
+  | ofNat _, negSucc _ => isFalse <| fun h => Int.noConfusion h
+  | negSucc _, ofNat _ => isFalse <| fun h => Int.noConfusion h
 
 instance : DecidableEq Int := Int.decEq
 
@@ -117,7 +117,7 @@ set_option bootstrap.genMatcherCode false in
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m   => isTrue <| NonNeg.mk m
-  | negSucc m => isFalse <| fun h => nomatch h
+  | negSucc _ => isFalse <| fun h => nomatch h
 
 @[extern "lean_int_dec_le"]
 instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
@@ -159,7 +159,7 @@ instance : Mod Int where
 
 def toNat : Int → Nat
   | ofNat n   => n
-  | negSucc n => 0
+  | negSucc _ => 0
 
 def natMod (m n : Int) : Nat := (m % n).toNat
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 96888e478a..0ae8df5792 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -89,14 +89,14 @@ theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as
 instance : EmptyCollection (List α) := ⟨List.nil⟩
 
 protected def erase {α} [BEq α] : List α → α → List α
-  | [],    b => []
+  | [],    _ => []
   | a::as, b => match a == b with
     | true  => as
     | false => a :: List.erase as b
 
 def eraseIdx : List α → Nat → List α
   | [],    _   => []
-  | a::as, 0   => as
+  | _::as, 0   => as
   | a::as, n+1 => a :: eraseIdx as n
 
 def isEmpty : List α → Bool
@@ -236,7 +236,7 @@ theorem mem_of_elem_eq_true [DecidableEq α] {a : α} {as : List α} : elem a as
 theorem elem_eq_true_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as = true := by
   induction h with
   | head _ => simp [elem]
-  | tail _ h ih => simp [elem]; split; rfl; assumption
+  | tail _ _ ih => simp [elem]; split; rfl; assumption
 
 instance [DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
@@ -303,12 +303,12 @@ def removeAll [BEq α] (xs ys : List α) : List α :=
 
 def drop : Nat → List α → List α
   | 0,   a     => a
-  | n+1, []    => []
-  | n+1, a::as => drop n as
+  | _+1, []    => []
+  | n+1, _::as => drop n as
 
 def take : Nat → List α → List α
-  | 0,   a     => []
-  | n+1, []    => []
+  | 0,   _     => []
+  | _+1, []    => []
   | n+1, a::as => a :: take n as
 
 def takeWhile (p : α → Bool) : List α → List α
@@ -368,14 +368,14 @@ theorem iota_eq_iotaTR : @iota = @iotaTR :=
   funext fun n => by simp [iotaTR, aux]
 
 def enumFrom : Nat → List α → List (Nat × α)
-  | n, [] => nil
+  | _, [] => nil
   | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs
 
 def enum : List α → List (Nat × α) := enumFrom 0
 
 def init : List α → List α
   | []   => []
-  | [a]  => []
+  | [_]  => []
   | a::l => a::init l
 
 def intersperse (sep : α) : List α → List α
@@ -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)
-  | [],    b::bs => isTrue (List.lt.nil _ _)
-  | a::as, []    => isFalse (fun h => nomatch h)
+  | [],    _::bs => isTrue (List.lt.nil _ _)
+  | _::as, []    => isFalse (fun h => nomatch h)
   | a::as, b::bs =>
     match h a b with
     | isTrue h₁  => isTrue (List.lt.head _ _ h₁)
@@ -420,8 +420,8 @@ instance hasDecidableLt [LT α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂
 
 instance [LT α] : LE (List α) := ⟨List.le⟩
 
-instance [LT α] [h : DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
-  fun a b => inferInstanceAs (Decidable (Not _))
+instance [LT α] [_ : DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
+  fun _ _ => inferInstanceAs (Decidable (Not _))
 
 /--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/
 def isPrefixOf [BEq α] : List α → List α → Bool
@@ -436,7 +436,7 @@ def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
 @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool
   | [],    [],    _   => true
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
-  | _,     _,     eqv => false
+  | _,     _,     _   => false
 
 protected def beq [BEq α] : List α → List α → Bool
   | [],    []    => true
@@ -446,7 +446,7 @@ protected def beq [BEq α] : List α → List α → Bool
 instance [BEq α] : BEq (List α) := ⟨List.beq⟩
 
 @[simp] def replicate : (n : Nat) → (a : α) → List α
-  | 0,   a => []
+  | 0,   _ => []
   | n+1, a => a :: replicate n a
 
 def replicateTR {α : Type u} (n : Nat) (a : α) : List α :=
@@ -466,7 +466,7 @@ theorem replicateTR_loop_replicate_eq (a : α) (m n : Nat) :
 
 def dropLast {α} : List α → List α
   | []    => []
-  | [a]   => []
+  | [_]   => []
   | a::as => a :: dropLast as
 
 @[simp] theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
@@ -475,7 +475,7 @@ def dropLast {α} : List α → List α
 @[simp] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
   induction as with
   | nil => rfl
-  | cons x xs ih => simp [concat, ih]
+  | cons _ xs ih => simp [concat, ih]
 
 @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by
   induction as generalizing i with
@@ -495,12 +495,12 @@ def dropLast {α} : List α → List α
 @[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
   induction as with
   | nil => simp
-  | cons a as ih => simp [ih, Nat.succ_add]
+  | cons _ as ih => simp [ih, Nat.succ_add]
 
 @[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by
   induction as with
   | nil => simp [List.map]
-  | cons a as ih => simp [List.map, ih]
+  | cons _ as ih => simp [List.map, ih]
 
 @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by
   induction as with
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index a33bd15e72..f75f626fcb 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -15,13 +15,13 @@ namespace List
    and `Init.Util` depends on `Init.Data.List.Basic`. -/
 
 def get! [Inhabited α] : List α → Nat → α
-  | a::as, 0   => a
-  | a::as, n+1 => get! as n
+  | a::_,  0   => a
+  | _::as, n+1 => get! as n
   | _,     _   => panic! "invalid index"
 
 def get? : List α → Nat → Option α
-  | a::as, 0   => some a
-  | a::as, n+1 => get? as n
+  | a::_,  0   => some a
+  | _::as, n+1 => get? as n
   | _,     _   => none
 
 def getD (as : List α) (idx : Nat) (a₀ : α) : α :=
@@ -44,20 +44,20 @@ def head : (as : List α) → as ≠ [] → α
 
 def tail! : List α → List α
   | []    => panic! "empty list"
-  | a::as => as
+  | _::as => as
 
 def tail? : List α → Option (List α)
   | []    => none
-  | a::as => some as
+  | _::as => some as
 
 def tailD : List α → List α → List α
   | [],   as₀ => as₀
-  | a::as, _  => as
+  | _::as, _  => as
 
 def getLast : ∀ (as : List α), as ≠ [] → α
   | [],       h => absurd rfl h
-  | [a],      h => a
-  | a::b::as, h => getLast (b::as) (fun h => List.noConfusion h)
+  | [a],      _ => a
+  | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h)
 
 def getLast! [Inhabited α] : List α → α
   | []    => panic! "empty list"
@@ -178,7 +178,7 @@ theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as
         have : a = b := s.antisymm hab hba
         simp [this, ih]
 
-instance [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
+instance [LT α] [_ : Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
 end List
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index d31a4008fa..3e58b27ff5 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -90,14 +90,14 @@ def filterMapM {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → m
 
 @[specialize]
 protected def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s → α → m s) → (init : s) → List α → m s
-  | f, s, []      => pure s
+  | _, s, []      => pure s
   | f, s, a :: as => do
     let s' ← f s a
     List.foldlM f s' as
 
 @[specialize]
 def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : α → s → m s) → (init : s) → List α → m s
-  | f, s, []      => pure s
+  | _, s, []      => pure s
   | f, s, a :: as => do
     let s' ← foldrM f s as
     f a s'
@@ -178,7 +178,7 @@ instance : ForIn' m (List α) α inferInstance where
 
 @[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by
   simp [forIn', forIn, List.forIn, List.forIn']
-  have : ∀ cs h, List.forIn'.loop cs (fun a x b => f a b) as init h = List.forIn.loop f as init := by
+  have : ∀ cs h, List.forIn'.loop cs (fun a _ b => f a b) as init h = List.forIn.loop f as init := by
     intro cs h
     induction as generalizing cs init with
     | nil => intros; rfl
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 10e963a3d5..fd2ac9cd63 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -82,7 +82,7 @@ instance : LawfulBEq Nat where
   | n+1 => congrArg succ (Nat.zero_add n)
 
 theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
-  | n, 0   => rfl
+  | _, 0   => rfl
   | n, m+1 => congrArg succ (succ_add n m)
 
 theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
@@ -102,7 +102,7 @@ protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
     apply this
 
 protected theorem add_assoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
-  | n, m, 0      => rfl
+  | _, _, 0      => rfl
   | n, m, succ k => congrArg succ (Nat.add_assoc n m k)
 
 protected theorem add_left_comm (n m k : Nat) : n + (m + k) = m + (n + k) := by
@@ -188,11 +188,11 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
 
 theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
-  | succ n => le_succ _
+  | succ _ => le_succ _
 
 theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
   | zero,   h => absurd rfl h
-  | succ n, h => lt_succ_of_le (Nat.le_refl _)
+  | succ _, _ => lt_succ_of_le (Nat.le_refl _)
 
 theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
@@ -200,9 +200,9 @@ theorem sub_le (n m : Nat) : n - m ≤ n := by
   | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
 
 theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
-  | 0,   m,   h1, h2 => absurd h1 (Nat.lt_irrefl 0)
-  | n+1, 0,   h1, h2 => absurd h2 (Nat.lt_irrefl 0)
-  | n+1, m+1, h1, h2 =>
+  | 0,   _,   h1, h2 => absurd h1 (Nat.lt_irrefl 0)
+  | _+1, 0,   h1, h2 => absurd h2 (Nat.lt_irrefl 0)
+  | n+1, m+1, _,  _  =>
     Eq.symm (succ_sub_succ_eq_sub n m) ▸
       show n - m < succ n from
       lt_succ_of_le (sub_le n m)
@@ -248,7 +248,7 @@ def lt.step {n m : Nat} : n < m → n < succ m := le_step
 
 theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
   | 0   => Or.inl rfl
-  | n+1 => Or.inr (succ_pos _)
+  | _+1 => Or.inr (succ_pos _)
 
 def lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
@@ -311,9 +311,9 @@ theorem le_add_left (n m : Nat): n ≤ m + n :=
   Nat.add_comm n m ▸ le_add_right n m
 
 theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
-  | zero,   zero,   h => ⟨0, rfl⟩
-  | zero,   succ n, h => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩
-  | succ n, zero,   h => absurd h (not_succ_le_zero _)
+  | zero,   zero,   _ => ⟨0, rfl⟩
+  | zero,   succ n, _ => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩
+  | succ _, zero,   h => absurd h (not_succ_le_zero _)
   | succ n, succ m, h =>
     have : n ≤ m := Nat.le_of_succ_le_succ h
     have : Exists (fun k => n + k = m) := dest this
@@ -519,7 +519,7 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
 
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
-  | 0, succ b, h => by simp
+  | 0, succ b, _ => by simp
   | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
   | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
 
diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index bf4ff6d8d5..38eede6222 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -119,7 +119,7 @@ theorem mod_one (x : Nat) : x % 1 = 0 := by
   have : (y : Nat) → y < 1 → y = 0 := by
     intro y
     cases y with
-    | zero   => intro h; rfl
+    | zero   => intro _; rfl
     | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
   exact this _ h
 
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index b482781b94..609aca1539 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -30,8 +30,8 @@ def Var.denote (ctx : Context) (v : Var) : Nat :=
   bif v == fixedVar then 1 else go ctx v
 where
   go : List Nat → Nat → Nat
-   | [],    i   => 0
-   | a::as, 0   => a
+   | [],    _   => 0
+   | a::_,  0   => a
    | _::as, i+1 => go as i
 
 inductive Expr where
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 6d9c6bbbb3..8792e47830 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -31,7 +31,7 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none,   _ => false
 
 @[inline] protected def bind : Option α → (α → Option β) → Option β
-  | none,   b => none
+  | none,   _ => none
   | some a, b => b a
 
 @[inline] protected def map (f : α → β) (o : Option α) : Option β :=
@@ -44,7 +44,7 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
     return none
 
 theorem map_id : (Option.map id : Option α → Option α) = id :=
-  funext (fun o => match o with | none => rfl | some x => rfl)
+  funext (fun o => match o with | none => rfl | some _ => rfl)
 
 instance : Functor Option where
   map := Option.map
@@ -69,14 +69,14 @@ instance : OrElse (Option α) where
   orElse := Option.orElse
 
 @[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
-  | none, some x     => True
+  | none, some _     => True
   | some x,   some y => r x y
   | _, _             => False
 
 instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
-  | none,   some y => isTrue  trivial
+  | none,   some _ => isTrue  trivial
   | some x, some y => s x y
-  | some x, none   => isFalse not_false
+  | some _, none   => isFalse not_false
   | none,   none   => isFalse not_false
 
 end Option
diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean
index a2eb044390..031bcadc70 100644
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -9,10 +9,10 @@ import Init.Data.Option.Basic
 universe u v
 
 theorem Option.eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀z, x = some z ↔ y = some z) → x = y
-  | none,   none,   h => rfl
+  | none,   none,   _ => rfl
   | none,   some z, h => Option.noConfusion ((h z).2 rfl)
   | some z, none,   h => Option.noConfusion ((h z).1 rfl)
-  | some z, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some)
+  | some _, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some)
 
 theorem Option.eq_none_of_isNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none
-  | none, h => rfl
+  | none, _ => rfl
diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean
index 84de67063d..42cec3efdd 100644
--- a/src/Init/Data/Random.lean
+++ b/src/Init/Data/Random.lean
@@ -84,7 +84,7 @@ The parameter `r` is the "remaining" magnitude.
 -/
 private partial def randNatAux {gen : Type u} [RandomGen gen] (genLo genMag : Nat) : Nat → (Nat × gen) → Nat × gen
   | 0,        (v, g) => (v, g)
-  | r'@(r+1), (v, g) =>
+  | r'@(_+1), (v, g) =>
     let (x, g') := RandomGen.next g
     let v'      := v*genMag + (x - genLo)
     randNatAux genLo genMag (r' / genMag - 1) (v', g')
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 40d2fb9ce7..3901cef9c8 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -29,7 +29,7 @@ abbrev reprArg [Repr α] (a : α) : Format :=
 
 /- Auxiliary class for marking types that should be considered atomic by `Repr` methods.
    We use it at `Repr (List α)` to decide whether `bracketFill` should be used or not. -/
-class ReprAtom (α : Type u)
+class ReprAtom (_ : Type u)
 
 -- This instance is needed because `id` is not reducible
 instance [Repr α] : Repr (id α) :=
@@ -62,7 +62,7 @@ instance [Repr α] : Repr (ULift.{v} α) where
     Repr.addAppParen ("ULift.up " ++ reprArg v.1) prec
 
 instance : Repr Unit where
-  reprPrec v _ := "()"
+  reprPrec _ _ := "()"
 
 instance [Repr α] : Repr (Option α) where
   reprPrec
@@ -88,7 +88,7 @@ instance [Repr α] [ReprTuple β] : ReprTuple (α × β) where
 instance [Repr α] [ReprTuple β] : Repr (α × β) where
   reprPrec | (a, b), _ => Format.bracket "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")"
 
-instance {β : α → Type v} [Repr α] [s : (x : α) → Repr (β x)] : Repr (Sigma β) where
+instance {β : α → Type v} [Repr α] [_ : (x : α) → Repr (β x)] : Repr (Sigma β) where
   reprPrec | ⟨a, b⟩, _ => Format.bracket "⟨" (repr a ++ ", " ++ repr b) "⟩"
 
 instance {p : α → Prop} [Repr α] : Repr (Subtype p) where
@@ -116,7 +116,7 @@ def digitChar (n : Nat) : Char :=
   '*'
 
 def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
-  | 0,      n, ds => ds
+  | 0,      _, ds => ds
   | fuel+1, n, ds =>
     let d  := digitChar <| n % base;
     let n' := n / base;
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 588646208a..dbe5880441 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -45,7 +45,7 @@ def toList (s : String) : List Char :=
   s.data
 
 private def utf8GetAux : List Char → Pos → Pos → Char
-  | [],    i, p => default
+  | [],    _, _ => default
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
 
 @[extern "lean_string_utf8_get"]
@@ -56,7 +56,7 @@ def getOp (self : String) (idx : Pos) : Char :=
   self.get idx
 
 private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
-  | [],    i, p => []
+  | [],    _, _ => []
   | c::cs, i, p =>
     if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
 
@@ -73,7 +73,7 @@ def next (s : @& String) (p : @& Pos) : Pos :=
   p + c
 
 private def utf8PrevAux : List Char → Pos → Pos → Pos
-  | [],    i, p => 0
+  | [],    _, _ => 0
   | c::cs, i, p =>
     let i' := i + c
     if i' = p then i else utf8PrevAux cs i' p
@@ -232,7 +232,7 @@ def remainingBytes : Iterator → Nat
   | ⟨s, i⟩ => s.endPos.byteIdx - i.byteIdx
 
 def pos : Iterator → Pos
-  | ⟨s, i⟩ => i
+  | ⟨_, i⟩ => i
 
 def curr : Iterator → Char
   | ⟨s, i⟩ => get s i
@@ -250,7 +250,7 @@ def hasNext : Iterator → Bool
   | ⟨s, i⟩ => i.byteIdx < s.endPos.byteIdx
 
 def hasPrev : Iterator → Bool
-  | ⟨s, i⟩ => i.byteIdx > 0
+  | ⟨_, i⟩ => i.byteIdx > 0
 
 def setCurr : Iterator → Char → Iterator
   | ⟨s, i⟩, c => ⟨s.set i c, i⟩
@@ -403,11 +403,11 @@ return the offset there of the previous codepoint. -/
     if absP = b then p else { byteIdx := (s.prev absP).byteIdx - b.byteIdx }
 
 def nextn : Substring → Nat → String.Pos → String.Pos
-  | ss, 0,   p => p
+  | _,  0,   p => p
   | ss, i+1, p => ss.nextn i (ss.next p)
 
 def prevn : Substring → Nat → String.Pos → String.Pos
-  | ss, 0,   p => p
+  | _,  0,   p => p
   | ss, i+1, p => ss.prevn i (ss.prev p)
 
 @[inline] def front (s : Substring) : Char :=
@@ -423,16 +423,16 @@ or `s.bsize` if `c` doesn't occur. -/
   | ss@⟨s, b, e⟩, n => ⟨s, b + ss.nextn n 0, e⟩
 
 @[inline] def dropRight : Substring → Nat → Substring
-  | ss@⟨s, b, e⟩, n => ⟨s, b, b + ss.prevn n ⟨ss.bsize⟩⟩
+  | ss@⟨s, b, _⟩, n => ⟨s, b, b + ss.prevn n ⟨ss.bsize⟩⟩
 
 @[inline] def take : Substring → Nat → Substring
-  | ss@⟨s, b, e⟩, n => ⟨s, b, b + ss.nextn n 0⟩
+  | ss@⟨s, b, _⟩, n => ⟨s, b, b + ss.nextn n 0⟩
 
 @[inline] def takeRight : Substring → Nat → Substring
   | ss@⟨s, b, e⟩, n => ⟨s, b + ss.prevn n ⟨ss.bsize⟩, e⟩
 
 @[inline] def atEnd : Substring → String.Pos → Bool
-  | ⟨s, b, e⟩, p => b + p == e
+  | ⟨_, b, e⟩, p => b + p == e
 
 @[inline] def extract : Substring → String.Pos → String.Pos → Substring
   | ⟨s, b, e⟩, b', e' => if b' ≥ e' then ⟨"", 0, 0⟩ else ⟨s, e.min (b+b'), e.min (b+e')⟩
diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index 6b632cbe77..6eed45023b 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@@ -46,7 +46,7 @@ instance {p : Prop} : ToString (Decidable p) := ⟨fun h =>
   | Decidable.isFalse _ => "false"⟩
 
 protected def List.toStringAux {α : Type u} [ToString α] : Bool → List α → String
-  | b,     []    => ""
+  | _,     []    => ""
   | true,  x::xs => toString x ++ List.toStringAux false xs
   | false, x::xs => ", " ++ toString x ++ List.toStringAux false xs
 
@@ -64,7 +64,7 @@ instance {α : Type u} [ToString α] : ToString (ULift.{v} α) :=
   ⟨fun v => toString v.1⟩
 
 instance : ToString Unit :=
-  ⟨fun u => "()"⟩
+  ⟨fun _ => "()"⟩
 
 instance : ToString Nat :=
   ⟨fun n => Nat.repr n⟩
@@ -117,7 +117,7 @@ instance {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (Sum
 instance {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (α × β) := ⟨fun (a, b) =>
   "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩
 
-instance {α : Type u} {β : α → Type v} [ToString α] [s : ∀ x, ToString (β x)] : ToString (Sigma β) := ⟨fun ⟨a, b⟩ =>
+instance {α : Type u} {β : α → Type v} [ToString α] [_ : ∀ x, ToString (β x)] : ToString (Sigma β) := ⟨fun ⟨a, b⟩ =>
   "⟨"  ++ toString a ++ ", " ++ toString b ++ "⟩"⟩
 
 instance {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p) := ⟨fun s =>
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index ae520a567d..480bbad1ae 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -106,7 +106,7 @@ def getRoot : Name → Name
 @[export lean_is_inaccessible_user_name]
 def isInaccessibleUserName : Name → Bool
   | Name.str _ s _   => s.contains '✝' || s == "_inaccessible"
-  | Name.num p idx _ => isInaccessibleUserName p
+  | Name.num p _   _ => isInaccessibleUserName p
   | _                => false
 
 def escapePart (s : String) : Option String :=
@@ -250,7 +250,7 @@ partial def getTailInfo? : Syntax → Option SourceInfo
   | ident info .. => info
   | node SourceInfo.none _ args =>
       args.findSomeRev? getTailInfo?
-  | node info _ args => info
+  | node info _ _    => info
   | _             => none
 
 def getTailInfo (stx : Syntax) : SourceInfo :=
@@ -291,7 +291,7 @@ partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
     match updateLast args (setTailInfoAux info) args.size with
     | some args => some <| node info k args
     | none      => none
-  | stx                    => none
+  | _                      => none
 
 def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
   match setTailInfoAux info stx with
@@ -318,8 +318,8 @@ partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
   | node i k args          =>
     match updateFirst args (setHeadInfoAux info) 0 with
     | some args => some <| node i k args
-    | noxne     => none
-  | stx                    => none
+    | _         => none
+  | _                      => none
 
 def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
   match setHeadInfoAux info stx with
@@ -787,7 +787,7 @@ private def getEscapedNameParts? (acc : List String) : Name → Option (List Str
   | Name.str n s _ => do
     let s ← Name.escapePart s
     getEscapedNameParts? (s::acc) n
-  | Name.num n i _ => none
+  | Name.num _ _ _ => none
 
 private def quoteNameMk : Name → Syntax
   | Name.anonymous => mkCIdent ``Name.anonymous
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e0913f7819..65f8830961 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -13,7 +13,7 @@ universe u v w
   fun x => f (g x)
 
 @[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
-  fun x => a
+  fun _ => a
 
 set_option checkBinderAnnotations false in
 @[reducible] def inferInstance {α : Sort u} [i : α] : α := i
@@ -109,8 +109,8 @@ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
 
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
   have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
-    fun α β a b h₁ =>
-      HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
+    fun α _ a _ h₁ =>
+      HEq.rec (motive := fun {β} (b : β) (_ : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
         (fun (h₂ : Eq α α) => rfl)
         h₁
   this α α a a' h rfl
@@ -171,7 +171,7 @@ structure Subtype {α : Sort u} (p : α → Prop) where
 @[reducible] def typedExpr (α : Sort u) (a : α) : α := a
 
 /-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/
-@[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
+@[reducible] def namedPattern {α : Sort u} (x a : α) (_ : Eq x a) : α := a
 
 /- Auxiliary axiom used to implement `sorry`. -/
 @[extern "lean_sorry", neverExtract]
@@ -179,10 +179,10 @@ axiom sorryAx (α : Sort u) (synthetic := false) : α
 
 theorem eq_false_of_ne_true : {b : Bool} → Not (Eq b true) → Eq b false
   | true, h => False.elim (h rfl)
-  | false, h => rfl
+  | false, _ => rfl
 
 theorem eq_true_of_ne_false : {b : Bool} → Not (Eq b false) → Eq b true
-  | true, h => rfl
+  | true, _ => rfl
   | false, h => False.elim (h rfl)
 
 theorem ne_false_of_eq_true : {b : Bool} → Eq b true → Not (Eq b false)
@@ -236,7 +236,7 @@ structure PLift (α : Sort u) : Type u where
 
 /- Bijection between α and PLift α -/
 theorem PLift.up_down {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b
-  | up a => rfl
+  | up _ => rfl
 
 theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a :=
   rfl
@@ -256,7 +256,7 @@ structure ULift.{r, s} (α : Type s) : Type (max s r) where
 
 /- Bijection between α and ULift.{v} α -/
 theorem ULift.up_down {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b
-  | up a => rfl
+  | up _ => rfl
 
 theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a :=
   rfl
@@ -282,13 +282,13 @@ abbrev DecidableEq (α : Sort u) :=
 def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (Eq a b) :=
   s a b
 
-theorem decide_eq_true : [s : Decidable p] → p → Eq (decide p) true
+theorem decide_eq_true : [_ : 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 h, _   => rfl
+  | isFalse _, _   => rfl
 
 theorem of_decide_eq_true [s : Decidable p] : Eq (decide p) true → p := fun h =>
   match (generalizing := false) s with
@@ -302,7 +302,7 @@ theorem of_decide_eq_false [s : Decidable p] : Eq (decide p) false → Not p :=
 
 theorem of_decide_eq_self_eq_true [s : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
   match (generalizing := false) s a a with
-  | isTrue  h₁ => rfl
+  | isTrue  _  => rfl
   | isFalse h₁ => absurd rfl h₁
 
 @[inline] instance : DecidableEq Bool :=
@@ -384,7 +384,7 @@ instance : Inhabited Nat where
   default := Nat.zero
 
 /- For numeric literals notation -/
-class OfNat (α : Type u) (n : Nat) where
+class OfNat (α : Type u) (_ : Nat) where
   ofNat : α
 
 @[defaultInstance 100] /- low prio -/
@@ -585,7 +585,7 @@ attribute [matchPattern] Nat.add Add.add HAdd.hAdd Neg.neg
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_nat_mul"]
 protected def Nat.mul : (@& Nat) → (@& Nat) → Nat
-  | a, 0          => 0
+  | _, 0          => 0
   | a, Nat.succ b => Nat.add (Nat.mul a b) a
 
 instance : Mul Nat where
@@ -604,26 +604,26 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_nat_dec_eq"]
 def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | zero,   zero   => true
-  | zero,   succ m => false
-  | succ n, zero   => false
+  | zero,   succ _ => false
+  | succ _, zero   => false
   | succ n, succ m => beq n m
 
 instance : BEq Nat where
   beq := Nat.beq
 
 theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
-  | zero,   zero,   h => rfl
-  | zero,   succ m, h => Bool.noConfusion h
-  | succ n, zero,   h => Bool.noConfusion h
+  | zero,   zero,   _ => rfl
+  | zero,   succ _, h => Bool.noConfusion h
+  | succ _, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
     have : Eq (beq n m) true := h
     have : Eq n m := eq_of_beq_eq_true this
     this ▸ rfl
 
 theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
-  | zero,   zero,   h₁, h₂ => Bool.noConfusion h₁
-  | zero,   succ m, h₁, h₂ => Nat.noConfusion h₂
-  | succ n, zero,   h₁, h₂ => Nat.noConfusion h₂
+  | zero,   zero,   h₁, _  => Bool.noConfusion h₁
+  | zero,   succ _, _,  h₂ => Nat.noConfusion h₂
+  | succ _, zero,   _,  h₂ => Nat.noConfusion h₂
   | succ n, succ m, h₁, h₂ =>
     have : Eq (beq n m) false := h₁
     Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this))
@@ -640,8 +640,8 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_nat_dec_le"]
 def Nat.ble : @& Nat → @& Nat → Bool
   | zero,   zero   => true
-  | zero,   succ m => true
-  | succ n, zero   => false
+  | zero,   succ _ => true
+  | succ _, zero   => false
   | succ n, succ m => ble n m
 
 protected inductive Nat.le (n : Nat) : Nat → Prop
@@ -659,7 +659,7 @@ instance : LT Nat where
 
 theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
   | 0,      h => nomatch h
-  | succ n, h => nomatch h
+  | succ _, h => nomatch h
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n
@@ -705,8 +705,8 @@ def Nat.pred : (@& Nat) → Nat
 
 theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m)
   | _,           _, Nat.le.refl   => Nat.le.refl
-  | 0,      succ m, Nat.le.step h => h
-  | succ n, succ m, Nat.le.step h => Nat.le_trans (le_succ _) h
+  | 0,      succ _, Nat.le.step h => h
+  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h
 
 theorem Nat.le_of_succ_le_succ {n m : Nat} : LE.le (succ n) (succ m) → LE.le n m :=
   pred_le_pred
@@ -715,9 +715,9 @@ theorem Nat.le_of_lt_succ {m n : Nat} : LT.lt m (succ n) → LE.le m n :=
   le_of_succ_le_succ
 
 protected theorem Nat.eq_or_lt_of_le : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.lt n m)
-  | zero,   zero,   h => Or.inl rfl
-  | zero,   succ n, h => Or.inr (Nat.succ_le_succ (Nat.zero_le _))
-  | succ n, zero,   h => absurd h (not_succ_le_zero _)
+  | zero,   zero,   _ => Or.inl rfl
+  | zero,   succ _, _ => Or.inr (Nat.succ_le_succ (Nat.zero_le _))
+  | succ _, zero,   h => absurd h (not_succ_le_zero _)
   | succ n, succ m, h =>
     have : LE.le n m := Nat.le_of_succ_le_succ h
     match Nat.eq_or_lt_of_le this with
@@ -755,7 +755,7 @@ protected theorem Nat.lt_of_le_of_ne {n m : Nat} (h₁ : LE.le n m) (h₂ : Not
   | Or.inl h₃ => h₃
   | Or.inr h₃ => absurd (Nat.le_antisymm h₁ h₃) h₂
 
-theorem Nat.le_of_ble_eq_true (h : Eq (Nat.ble n m) true) : LE.le n m :=
+theorem Nat.le_of_ble_eq_true (_ : Eq (Nat.ble n m) true) : LE.le n m :=
   match n, m with
   | 0,      _      => Nat.zero_le _
   | succ _, succ _ => Nat.succ_le_succ (le_of_ble_eq_true h)
@@ -766,7 +766,7 @@ theorem Nat.ble_self_eq_true : (n : Nat) → Eq (Nat.ble n n) true
 
 theorem Nat.ble_succ_eq_true : {n m : Nat} → Eq (Nat.ble n m) true → Eq (Nat.ble n (succ m)) true
   | 0,      _,      _ => rfl
-  | succ n, succ m, h => ble_succ_eq_true (n := n) h
+  | succ n, succ _, h => ble_succ_eq_true (n := n) h
 
 theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
   match h with
@@ -807,7 +807,7 @@ structure Fin (n : Nat) where
   isLt : LT.lt val n
 
 theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
-  | ⟨v, h⟩, ⟨_, _⟩, rfl => rfl
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 theorem Fin.val_eq_of_eq {n} {i j : Fin n} (h : Eq i j) : Eq i.val j.val :=
   h ▸ rfl
@@ -1021,7 +1021,7 @@ def Char.ofNat (n : Nat) : Char :=
     (fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })
 
 theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
-  | ⟨v, h⟩, ⟨_, _⟩, rfl => rfl
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 theorem Char.val_eq_of_eq : ∀ {c d : Char}, Eq c d → Eq c.val d.val
   | _, _, rfl => rfl
@@ -1072,8 +1072,8 @@ instance {α} : Inhabited (List α) where
 
 protected def List.hasDecEq {α: Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
   | nil,       nil       => isTrue rfl
-  | cons a as, nil       => isFalse (fun h => List.noConfusion h)
-  | nil,       cons b bs => isFalse (fun h => List.noConfusion h)
+  | cons _ as, nil       => isFalse (fun h => List.noConfusion h)
+  | nil,       cons _ bs => isFalse (fun h => List.noConfusion h)
   | cons a as, cons b bs =>
     match decEq a b with
     | isTrue hab  =>
@@ -1090,17 +1090,17 @@ def List.foldl {α β} (f : α → β → α) : (init : α) → List β → α
   | a, cons b l => foldl f (f a b) l
 
 def List.set : List α → Nat → α → List α
-  | cons a as, 0,          b => cons b as
+  | cons _ as, 0,          b => cons b as
   | cons a as, Nat.succ n, b => cons a (set as n b)
   | nil,       _,          _ => nil
 
 def List.length : List α → Nat
   | nil       => 0
-  | cons a as => HAdd.hAdd (length as) 1
+  | cons _ as => HAdd.hAdd (length as) 1
 
 def List.lengthTRAux : List α → Nat → Nat
   | nil,       n => n
-  | cons a as, n => lengthTRAux as (Nat.succ n)
+  | cons _ as, n => lengthTRAux as (Nat.succ n)
 
 def List.lengthTR (as : List α) : Nat :=
   lengthTRAux as 0
@@ -1113,8 +1113,8 @@ def List.concat {α : Type u} : List α → α → List α
   | cons a as, b => cons a (concat as b)
 
 def List.get {α : Type u} : (as : List α) → Fin as.length → α
-  | cons a as, ⟨0, _⟩ => a
-  | cons a as, ⟨Nat.succ i, h⟩ => get as ⟨i, Nat.le_of_succ_le_succ h⟩
+  | cons a _,  ⟨0, _⟩ => a
+  | cons _ as, ⟨Nat.succ i, h⟩ => get as ⟨i, Nat.le_of_succ_le_succ h⟩
 
 structure String where
   data : List Char
@@ -1469,7 +1469,7 @@ variable {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}
   pure
 
 @[inline] protected def pure (a : α) : ReaderT ρ m α :=
-  fun r => pure a
+  fun _ => pure a
 
 @[inline] protected def bind (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β :=
   fun r => bind (x r) fun a => f a r
@@ -1739,8 +1739,8 @@ instance : Inhabited Name where
 
 protected def Name.hash : Name → UInt64
   | Name.anonymous => UInt64.ofNatCore 1723 (by decide)
-  | Name.str p s h => h
-  | Name.num p v h => h
+  | Name.str _ _ h => h
+  | Name.num _ _ h => h
 
 instance : Hashable Name where
   hash := Name.hash
@@ -1860,7 +1860,7 @@ namespace Syntax
 
 def getKind (stx : Syntax) : SyntaxNodeKind :=
   match stx with
-  | Syntax.node _ k args => k
+  | Syntax.node _ k _    => k
   -- We use these "pseudo kinds" for antiquotation kinds.
   -- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident)
   -- is compiled to ``if stx.isOfKind `ident ...``
@@ -2139,7 +2139,7 @@ private def assembleParts : List Name → Name → Name
   | List.nil,                      acc => acc
   | List.cons (Name.str _ s _) ps, acc => assembleParts ps (Name.mkStr acc s)
   | List.cons (Name.num _ n _) ps, acc => assembleParts ps (Name.mkNum acc n)
-  | _,                             acc => panic "Error: unreachable @ assembleParts"
+  | _,                             _   => panic "Error: unreachable @ assembleParts"
 
 private def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView
   | n@(Name.str p str _), parts =>
@@ -2154,12 +2154,12 @@ private def extractMainModule (scps : List MacroScope) : Name → List Name →
     match beq str "_@" with
     | true  => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
     | false => extractMainModule scps p (List.cons n parts)
-  | n@(Name.num p num _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
+  | n@(Name.num _ num _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
   | _,                    _   => panic "Error: unreachable @ extractMainModule"
 
 private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
   | Name.num p scp _, acc => extractMacroScopesAux p (List.cons scp acc)
-  | Name.str p str _, acc => extractMainModule acc p List.nil -- str must be "_hyg"
+  | Name.str p _   _, acc => extractMainModule acc p List.nil -- str must be "_hyg"
   | _,                _   => panic "Error: unreachable @ extractMacroScopesAux"
 
 /--
diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index 9a1914c021..a5fddd498b 100644
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -23,10 +23,10 @@ theorem eq_false (h : ¬ p) : p = False :=
 theorem eq_false' (h : p → False) : p = False :=
   propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
 
-theorem eq_true_of_decide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True :=
-  propext <| Iff.intro (fun h => trivial) (fun _ => of_decide_eq_true h)
+theorem eq_true_of_decide {p : Prop} {_ : Decidable p} (h : decide p = true) : p = True :=
+  propext <| Iff.intro (fun _ => trivial) (fun _ => of_decide_eq_true h)
 
-theorem eq_false_of_decide {p : Prop} {s : Decidable p} (h : decide p = false) : p = False :=
+theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) : p = False :=
   propext <| Iff.intro (fun h' => absurd h' (of_decide_eq_false h)) (fun h => False.elim h)
 
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
@@ -105,11 +105,11 @@ theorem dite_congr {s : Decidable b} [Decidable c]
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := propext <| Iff.intro (fun h => h.2) (fun h => False.elim h)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := propext <| Iff.intro (fun h => h.1) (fun h => False.elim h)
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext <| Iff.intro (fun | Or.inl h => h | Or.inr h => h) (fun h => Or.inl h)
-@[simp] theorem or_true (p : Prop) : (p ∨ True) = True := propext <| Iff.intro (fun h => trivial) (fun h => Or.inr trivial)
-@[simp] theorem true_or (p : Prop) : (True ∨ p) = True := propext <| Iff.intro (fun h => trivial) (fun h => Or.inl trivial)
+@[simp] theorem or_true (p : Prop) : (p ∨ True) = True := propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
+@[simp] theorem true_or (p : Prop) : (True ∨ p) = True := propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inl trivial)
 @[simp] theorem or_false (p : Prop) : (p ∨ False) = p := propext <| Iff.intro (fun | Or.inl h => h | Or.inr h => False.elim h) (fun h => Or.inl h)
 @[simp] theorem false_or (p : Prop) : (False ∨ p) = p := propext <| Iff.intro (fun | Or.inr h => h | Or.inl h => False.elim h) (fun h => Or.inr h)
-@[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := propext <| Iff.intro (fun h => trivial) (fun _ => Iff.intro id id)
+@[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := propext <| Iff.intro (fun _ => trivial) (fun _ => Iff.intro id id)
 @[simp] theorem iff_true (p : Prop) : (p ↔ True) = p := propext <| Iff.intro (fun h => h.mpr trivial) (fun h => Iff.intro (fun _ => trivial) (fun _ => h))
 @[simp] theorem true_iff (p : Prop) : (True ↔ p) = p := propext <| Iff.intro (fun h => h.mp trivial) (fun h => Iff.intro (fun _ => h) (fun _ => trivial))
 @[simp] theorem iff_false (p : Prop) : (p ↔ False) = ¬p := propext <| Iff.intro (fun h hp => h.mp hp) (fun h => Iff.intro h False.elim)
diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean
index c671697e17..84e517d879 100644
--- a/src/Init/SizeOf.lean
+++ b/src/Init/SizeOf.lean
@@ -20,7 +20,7 @@ From now on, the inductive Compiler will automatically generate sizeOf instances
 
 /- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/
 protected def default.sizeOf (α : Sort u) : α → Nat
-  | a => 0
+  | _ => 0
 
 instance (priority := low) (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index da2b65cf2c..ef5b7ec1f7 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -17,7 +17,7 @@ instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) :=
 instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
 
 -- Auxiliary class for inferring the "state" of `EST` and `ST` monads
-class STWorld (σ : outParam Type) (m : Type → Type)
+class STWorld (_ : outParam Type) (_ : Type → Type)
 
 instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
 instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
@@ -44,7 +44,7 @@ namespace ST
 /- References -/
 constant RefPointed : NonemptyType.{0}
 
-structure Ref (σ : Type) (α : Type) : Type where
+structure Ref (_ : Type) (α : Type) : Type where
   ref : RefPointed.type
   h   : Nonempty α
 
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index a5ad3639aa..7b84caf67f 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -384,7 +384,7 @@ syntax (name := dbgTrace) "dbg_trace " str : tactic
 
 /-- `stop` is a helper tactic for "discarding" the rest of a proof. It is useful when working on the middle of a complex proofs,
     and less messy than commenting the remainder of the proof. -/
-macro "stop" s:tacticSeq : tactic => `(repeat sorry)
+macro "stop" _:tacticSeq : tactic => `(repeat sorry)
 
 /--
 The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`.
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 8a8bb7c094..d3f18b4fe4 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -10,14 +10,14 @@ import Init.Data.ToString.Basic
 universe u v
 /- debugging helper functions -/
 @[neverExtract, extern "lean_dbg_trace"]
-def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α := f ()
+def dbgTrace {α : Type u} (_ : String) (f : Unit → α) : α := f ()
 
 def dbgTraceVal {α : Type u} [ToString α] (a : α) : α :=
   dbgTrace (toString a) (fun _ => a)
 
 /- Display the given message if `a` is shared, that is, RC(a) > 1 -/
 @[neverExtract, extern "lean_dbg_trace_if_shared"]
-def dbgTraceIfShared {α : Type u} (s : String) (a : α) : α := a
+def dbgTraceIfShared {α : Type u} (_ : String) (a : α) : α := a
 
 @[extern "lean_dbg_sleep"]
 def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
@@ -37,10 +37,10 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[extern "lean_ptr_addr"]
 unsafe def ptrAddrUnsafe {α : Type u} (a : @& α) : USize := 0
 
-@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
+@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (_ : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)
 
-@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
+@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (_ : a = b → k () = true) : Bool :=
   if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
 
 @[implementedBy withPtrEqUnsafe]
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 5e71e5fb20..8a1b9f3451 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -43,7 +43,7 @@ class WellFoundedRelation (α : Sort u) where
 
 namespace WellFounded
 def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
-  WellFounded.recOn (motive := fun x => (y : α) → Acc r y)
+  WellFounded.recOn (motive := fun _ => (y : α) → Acc r y)
     wf (fun p => p) a
 
 section
@@ -51,7 +51,7 @@ variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
 
 theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
   induction (apply hwf a) with
-  | intro x₁ ac₁ ih => exact h x₁ ih
+  | intro x₁ _   ih => exact h x₁ ih
 
 theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
   recursion hwf a h
@@ -62,11 +62,11 @@ variable (F : ∀ x, (∀ y, r y x → C y) → C x)
 set_option codegen false in
 def fixF (x : α) (a : Acc r x) : C x := by
   induction a with
-  | intro x₁ ac₁ ih => exact F x₁ ih
+  | intro x₁ _   ih => exact F x₁ ih
 
 def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
   induction acx with
-  | intro x r ih => exact rfl
+  | intro x r _  => exact rfl
 
 end
 
@@ -79,7 +79,7 @@ def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : 
 
 -- Well-founded fixpoint satisfies fixpoint equation
 theorem fix_eq (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) :
-    fix hwf F x = F x (fun y h => fix hwf F y) :=
+    fix hwf F x = F x (fun y _ => fix hwf F y) :=
   fixFEq F x (apply hwf x)
 end WellFounded
 
@@ -101,7 +101,7 @@ variable {α : Sort u} {r q : α → α → Prop}
 
 def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
   induction ac with
-  | intro x ax ih =>
+  | intro x _  ih =>
     apply Acc.intro
     intro y h
     exact ih y (h₁ h)
@@ -216,9 +216,9 @@ variable {ra  : α → α → Prop} {rb  : β → β → Prop}
 
 def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
   induction (aca a) generalizing b with
-  | intro xa aca iha =>
+  | intro xa _   iha =>
     induction (acb b) with
-    | intro xb acb ihb =>
+    | intro xb _   ihb =>
       apply Acc.intro (xa, xb)
       intro p lt
       cases lt with
@@ -268,9 +268,9 @@ variable {r  : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop}
 
 def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
   induction aca with
-  | intro xa aca iha =>
+  | intro xa _   iha =>
     induction (WellFounded.apply (acb xa) b) with
-    | intro xb acb ihb =>
+    | intro xb _   ihb =>
       apply Acc.intro
       intro p lt
       cases lt with
@@ -291,17 +291,17 @@ section
 variable {α : Sort u} {β : Sort v}
 
 def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
-  Lex r (fun a => s)
+  Lex r (fun _ => s)
 
 def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
-  WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
+  WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
 end
 
 section
 variable {α : Sort u} {β : Sort v}
 
 -- Reverse lexicographical order based on r and s
-inductive RevLex (r  : α → α → Prop) (s  : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop where
+inductive RevLex (r  : α → α → Prop) (s  : β → β → Prop) : @PSigma α (fun _ => β) → @PSigma α (fun _ => β) → Prop where
   | left  : {a₁ a₂ : α} → (b : β) → r a₁ a₂ → RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
   | right : (a₁ : α) → {b₁ : β} → (a₂ : α) → {b₂ : β} → s b₁ b₂ → RevLex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
 end
@@ -313,10 +313,10 @@ variable {r  : α → α → Prop} {s : β → β → Prop}
 
 def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
   induction acb with
-  | intro xb acb ihb =>
+  | intro xb _   ihb =>
     intro a
     induction (aca a) with
-    | intro xa aca iha =>
+    | intro xa _   iha =>
       apply Acc.intro
       intro p lt
       cases lt with
@@ -328,10 +328,10 @@ def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s)
 end
 
 section
-def SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop :=
+def SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (fun _ => β) → @PSigma α (fun _ => β) → Prop :=
   RevLex emptyRelation s
 
-def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation (PSigma fun a : α => β) where
+def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation (PSigma fun _ : α => β) where
   rel := SkipLeft α hb.rel
   wf  := revLex emptyWf.wf hb.wf
 
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 667e547cfa..1841458bd9 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -74,7 +74,7 @@ private partial def checkOutParam : Nat → Array FVarId → Expr → Except Str
       Except.error s!"invalid class, parameter #{i} depends on `outParam`, but it is not an `outParam`"
     else
       checkOutParam (i+1) outParams b
-  | i, outParams, e => pure (outParams.size > 0)
+  | _, outParams, _ => pure (outParams.size > 0)
 
 def addClass (env : Environment) (clsName : Name) : Except String Environment := do
   if isClass env clsName then
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index ed9fc54602..8b8bc43bc0 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -87,7 +87,7 @@ private def parseOptNum : Nat → String.Iterator → Nat → String.Iterator ×
       else (it, r)
 
 def expandExternPatternAux (args : List String) : Nat → String.Iterator → String → String
-  | 0,   it, r => r
+  | 0,   _,  r => r
   | i+1, it, r =>
     if ¬ it.hasNext then r
     else let c := it.curr
@@ -156,7 +156,7 @@ def getExternConstArityExport (env : Environment) (declName : Name) : IO (Option
     let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default } { env := env }
     return some arity
   catch
-   | IO.Error.userError msg => return none
+   | IO.Error.userError _   => return none
    | _  => return none
 
 end Lean
diff --git a/src/Lean/Compiler/IR.lean b/src/Lean/Compiler/IR.lean
index d62132b4fb..9fa9939315 100644
--- a/src/Lean/Compiler/IR.lean
+++ b/src/Lean/Compiler/IR.lean
@@ -82,6 +82,6 @@ def addBoxedVersionAux (decl : Decl) : CompilerM Unit := do
 def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environment :=
   match (addBoxedVersionAux decl Options.empty).run { env := env } with
   | EStateM.Result.ok     _  s => Except.ok s.env
-  | EStateM.Result.error msg s => Except.error msg
+  | EStateM.Result.error msg _ => Except.error msg
 
 end Lean.IR
diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index ed4bf35027..a56b4abde6 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -326,7 +326,7 @@ def FnBody.setBody : FnBody → FnBody → FnBody
   | FnBody.dec x n c p _,    b => FnBody.dec x n c p b
   | FnBody.del x _,          b => FnBody.del x b
   | FnBody.mdata d _,        b => FnBody.mdata d b
-  | other,                   b => other
+  | other,                   _ => other
 
 @[inline] def FnBody.resetBody (b : FnBody) : FnBody :=
   b.setBody FnBody.nil
@@ -427,7 +427,7 @@ def getInfo : Decl → DeclInfo
 
 def updateBody! (d : Decl) (bNew : FnBody) : Decl :=
   match d with
-  | Decl.fdecl f xs t b info => Decl.fdecl f xs t bNew info
+  | Decl.fdecl f xs t _ info => Decl.fdecl f xs t bNew info
   | _ => panic! "expected definition"
 
 end Decl
@@ -473,27 +473,27 @@ def LocalContext.addParams (ctx : LocalContext) (ps : Array Param) : LocalContex
 def LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool :=
   match ctx.find? idx with
   | some (LocalContextEntry.joinPoint _ _) => true
-  | other => false
+  | _     => false
 
 def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody :=
   match ctx.find? j.idx with
   | some (LocalContextEntry.joinPoint _ b) => some b
-  | other => none
+  | _     => none
 
 def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) :=
   match ctx.find? j.idx with
   | some (LocalContextEntry.joinPoint ys _) => some ys
-  | other => none
+  | _     => none
 
 def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool :=
   match ctx.find? idx with
   | some (LocalContextEntry.param _) => true
-  | other => false
+  | _     => false
 
 def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool :=
   match ctx.find? idx with
   | some (LocalContextEntry.localVar _ _) => true
-  | other => false
+  | _     => false
 
 def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool :=
   Std.RBMap.contains ctx idx
@@ -505,12 +505,12 @@ def LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType :=
   match ctx.find? x.idx with
   | some (LocalContextEntry.param t) => some t
   | some (LocalContextEntry.localVar t _) => some t
-  | other => none
+  | _     => none
 
 def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr :=
   match ctx.find? x.idx with
   | some (LocalContextEntry.localVar _ v) => some v
-  | other => none
+  | _     => none
 
 abbrev IndexRenaming := RBMap Index Index compare
 
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index 253c77ba87..34c1364c76 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -105,7 +105,7 @@ def mkInitParamMap (env : Environment) (decls : Array Decl) : ParamMap :=
 namespace ApplyParamMap
 
 partial def visitFnBody (fn : FunId) (paramMap : ParamMap) : FnBody → FnBody
-  | FnBody.jdecl j xs v b =>
+  | FnBody.jdecl j _  v b =>
     let v := visitFnBody fn paramMap v
     let b := visitFnBody fn paramMap b
     match paramMap.find? (ParamMap.Key.jp fn j) with
@@ -122,7 +122,7 @@ partial def visitFnBody (fn : FunId) (paramMap : ParamMap) : FnBody → FnBody
 
 def visitDecls (decls : Array Decl) (paramMap : ParamMap) : Array Decl :=
   decls.map fun decl => match decl with
-    | Decl.fdecl f xs ty b info =>
+    | Decl.fdecl f _  ty b info =>
       let b := visitFnBody f paramMap b
       match paramMap.find? (ParamMap.Key.decl f) with
       | some xs => Decl.fdecl f xs ty b info
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index d31f231617..e6e657698c 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -290,7 +290,7 @@ def visitVDeclExpr (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : M FnBody
   | Expr.ap f ys =>
     boxArgsIfNeeded ys fun ys =>
     unboxResultIfNeeded x ty (Expr.ap f ys) b
-  | other =>
+  | _     =>
     return FnBody.vdecl x ty e b
 
 partial def visitFnBody : FnBody → M FnBody
diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index ae0d7e6758..45f8c92b8f 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -120,7 +120,7 @@ def checkExpr (ty : IRType) : Expr → M Unit
     if !ty.isStruct && !ty.isUnion && c.isRef then
       (checkObjType ty) *> checkArgs ys
   | Expr.reset _ x          => checkObjVar x *> checkObjType ty
-  | Expr.reuse x i u ys     => checkObjVar x *> checkArgs ys *> checkObjType ty
+  | Expr.reuse x _ _ ys     => checkObjVar x *> checkArgs ys *> checkObjType ty
   | Expr.box xty x          => checkObjType ty *> checkScalarVar x *> checkVarType x (fun t => t == xty)
   | Expr.unbox x            => checkScalarType ty *> checkObjVar x
   | Expr.proj i x           => do
@@ -130,7 +130,7 @@ def checkExpr (ty : IRType) : Expr → M Unit
     | IRType.tobject      => checkObjType ty
     | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
     | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
-    | other               => throw s!"unexpected IR type '{xType}'"
+    | _                   => throw s!"unexpected IR type '{xType}'"
   | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
   | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty
   | Expr.isShared x         => checkObjVar x *> checkType ty (fun t => t == IRType.uint8)
diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean
index 65dc2514af..4371ca8351 100644
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -45,7 +45,7 @@ def tracePrefixOptionName := `trace.compiler.ir
 private def isLogEnabledFor (opts : Options) (optName : Name) : Bool :=
   match opts.find optName with
   | some (DataValue.ofBool v) => v
-  | other => opts.getBool tracePrefixOptionName
+  | _     => opts.getBool tracePrefixOptionName
 
 private def logDeclsAux (optName : Name) (cls : Name) (decls : Array Decl) : CompilerM Unit := do
   let opts ← read
@@ -79,7 +79,7 @@ private def mkEntryArray (decls : List Decl) : Array Decl :=
   /- Remove duplicates by adding decls into a map -/
   let map : HashMap Name Decl := {}
   let map := decls.foldl (init := map) fun map decl => map.insert decl.name decl
-  map.fold (fun a k v => a.push v) #[]
+  map.fold (fun a _ v => a.push v) #[]
 
 builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
   registerSimplePersistentEnvExtension {
diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean
index 485781a979..faa7d0525e 100644
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -186,7 +186,7 @@ partial def projValue : Value → Nat → Value
 def interpExpr : Expr → M Value
   | Expr.ctor i ys => return ctor i (← ys.mapM fun y => findArgValue y)
   | Expr.proj i x  => return projValue (← findVarValue x) i
-  | Expr.fap fid ys => do
+  | Expr.fap fid _  => do
     let ctx ← read
     match getFunctionSummary? ctx.env fid with
     | some v => pure v
@@ -225,7 +225,7 @@ def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
       pure true
 
 private partial def resetNestedJPParams : FnBody → M Unit
-  | FnBody.jdecl _ ys b k => do
+  | FnBody.jdecl _ ys _ k => do
     let ctx ← read
     let currFnIdx := ctx.currFnIdx
     ys.forM resetParamAssignment
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 6a11e7bd3a..d8d409dc54 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -138,7 +138,7 @@ def emitFnDecls : M Unit := do
 def emitMainFn : M Unit := do
   let d ← getDecl `main
   match d with
-  | Decl.fdecl (f := f) (xs := xs) (type := t) (body := b) .. => do
+  | Decl.fdecl (f := _) (xs := xs) (type := _) (body := _) .. => do
     unless xs.size == 2 || xs.size == 1 do throw "invalid main function, incorrect arity when generating code"
     let env ← getEnv
     let usesLeanAPI := usesModuleFrom env `Lean
@@ -199,7 +199,7 @@ def emitMainFn : M Unit := do
              "  return 1;",
              "}"]
     emitLn "}"
-  | other => throw "function declaration expected"
+  | _     => throw "function declaration expected"
 
 def hasMainFn : M Bool := do
   let env ← getEnv
@@ -261,7 +261,7 @@ partial def declareVars : FnBody → Bool → M Bool
       pure d
     else
       declareVar x t; declareVars b true
-  | FnBody.jdecl j xs _ b,    d => do declareParams xs; declareVars b (d || xs.size > 0)
+  | FnBody.jdecl _ xs _ b,    d => do declareParams xs; declareVars b (d || xs.size > 0)
   | e,                        d => if e.isTerminal then pure d else declareVars e.body d
 
 def emitTag (x : VarId) (xType : IRType) : M Unit := do
@@ -448,7 +448,7 @@ def emitBoxFn (xType : IRType) : M Unit :=
   | IRType.uint32 => emit "lean_box_uint32"
   | IRType.uint64 => emit "lean_box_uint64"
   | IRType.float  => emit "lean_box_float"
-  | other         => emit "lean_box"
+  | _             => emit "lean_box"
 
 def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do
   emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");"
@@ -460,7 +460,7 @@ def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do
   | IRType.uint32 => emit "lean_unbox_uint32"
   | IRType.uint64 => emit "lean_unbox_uint64"
   | IRType.float  => emit "lean_unbox_float"
-  | other         => emit "lean_unbox";
+  | _             => emit "lean_unbox";
   emit "("; emit x; emitLn ");"
 
 def emitIsShared (z : VarId) (x : VarId) : M Unit := do
@@ -600,7 +600,7 @@ partial def emitCase (x : VarId) (xType : IRType) (alts : Array Alt) : M Unit :=
 
 partial def emitBlock (b : FnBody) : M Unit := do
   match b with
-  | FnBody.jdecl j xs v b      => emitBlock b
+  | FnBody.jdecl _ _  _ b      => emitBlock b
   | d@(FnBody.vdecl x t v b)   =>
     let ctx ← read
     if isTailCallTo ctx.mainFn d then
@@ -626,7 +626,7 @@ partial def emitBlock (b : FnBody) : M Unit := do
   | FnBody.unreachable         => emitLn "lean_internal_panic_unreachable();"
 
 partial def emitJPs : FnBody → M Unit
-  | FnBody.jdecl j xs v b => do emit j; emitLn ":"; emitFnBody v; emitJPs b
+  | FnBody.jdecl j _  v b => do emit j; emitLn ":"; emitFnBody v; emitJPs b
   | e                     => do unless e.isTerminal do emitJPs e.body
 
 partial def emitFnBody (b : FnBody) : M Unit := do
diff --git a/src/Lean/Compiler/IR/EmitUtil.lean b/src/Lean/Compiler/IR/EmitUtil.lean
index 0b798abfce..86b1922ae0 100644
--- a/src/Lean/Compiler/IR/EmitUtil.lean
+++ b/src/Lean/Compiler/IR/EmitUtil.lean
@@ -30,7 +30,7 @@ partial def collectFnBody : FnBody → M Unit
     match v with
     | Expr.fap f _ => collect f *> collectFnBody b
     | Expr.pap f _ => collect f *> collectFnBody b
-    | other        => collectFnBody b
+    | _            => collectFnBody b
   | FnBody.jdecl _ _ v b   => collectFnBody v *> collectFnBody b
   | FnBody.case _ _ _ alts => alts.forM fun alt => collectFnBody alt.body
   | e => do unless e.isTerminal do collectFnBody e.body
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index 8294b7d024..a6d3816999 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -93,7 +93,7 @@ partial def reuseToCtor (x : VarId) : FnBody → FnBody
     else FnBody.dec y n c p (reuseToCtor x b)
   | FnBody.vdecl z t v b   =>
     match v with
-    | Expr.reuse y c u xs =>
+    | Expr.reuse y c _ xs =>
       if x == y then FnBody.vdecl z t (Expr.ctor c xs) b
       else FnBody.vdecl z t v (reuseToCtor x b)
     | _ =>
@@ -248,7 +248,7 @@ partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
   return reshape bs b
 
 partial def searchAndExpand : FnBody → Array FnBody → M FnBody
-  | d@(FnBody.vdecl x t (Expr.reset n y) b), bs =>
+  | d@(FnBody.vdecl x _ (Expr.reset n y) b), bs =>
     if consumed x b then do
       expand searchAndExpand bs x n y b
     else
diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index 6e94560b31..f06042663b 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -87,17 +87,17 @@ def formatParams (ps : Array Param) : Format :=
 
 @[export lean_ir_format_fn_body_head]
 def formatFnBodyHead : FnBody → Format
-  | FnBody.vdecl x ty e b      => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e
-  | FnBody.jdecl j xs v b      => format j ++ formatParams xs ++ " := ..."
-  | FnBody.set x i y b         => "set " ++ format x ++ "[" ++ format i ++ "] := " ++ format y
-  | FnBody.uset x i y b        => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y
-  | FnBody.sset x i o y ty b   => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y
-  | FnBody.setTag x cidx b     => "setTag " ++ format x ++ " := " ++ format cidx
-  | FnBody.inc x n c _ b       => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
-  | FnBody.dec x n c _ b       => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
-  | FnBody.del x b             => "del " ++ format x
-  | FnBody.mdata d b           => "mdata " ++ format d
-  | FnBody.case tid x xType cs => "case " ++ format x ++ " of ..."
+  | FnBody.vdecl x ty e _      => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e
+  | FnBody.jdecl j xs _ _      => format j ++ formatParams xs ++ " := ..."
+  | FnBody.set x i y _         => "set " ++ format x ++ "[" ++ format i ++ "] := " ++ format y
+  | FnBody.uset x i y _        => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y
+  | FnBody.sset x i o y ty _   => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y
+  | FnBody.setTag x cidx _     => "setTag " ++ format x ++ " := " ++ format cidx
+  | FnBody.inc x n _ _ _       => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
+  | FnBody.dec x n _ _ _       => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
+  | FnBody.del x _             => "del " ++ format x
+  | FnBody.mdata d _           => "mdata " ++ format d
+  | FnBody.case _   x _     _  => "case " ++ format x ++ " of ..."
   | FnBody.jmp j ys            => "jmp " ++ format j ++ formatArray ys
   | FnBody.ret x               => "ret " ++ format x
   | FnBody.unreachable         => "⊥"
@@ -110,8 +110,8 @@ partial def formatFnBody (fnBody : FnBody) (indent : Nat := 2) : Format :=
     | FnBody.uset x i y b        => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ loop b
     | FnBody.sset x i o y ty b   => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y ++ ";" ++ Format.line ++ loop b
     | FnBody.setTag x cidx b     => "setTag " ++ format x ++ " := " ++ format cidx ++ ";" ++ Format.line ++ loop b
-    | FnBody.inc x n c _ b       => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
-    | FnBody.dec x n c _ b       => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
+    | FnBody.inc x n _ _ b       => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
+    | 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
diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean
index 35d8fc617e..5e18318c5c 100644
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -28,7 +28,7 @@ instance : AndThen Collector where
 
 private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
-  | irrelevant => skip
+  | _          => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun m => as.foldl (fun m a => f a m) m
@@ -49,7 +49,7 @@ private def collectExpr : Expr → Collector
   | Expr.ap x ys        => collectVar x >> collectArgs ys
   | Expr.box _ x        => collectVar x
   | Expr.unbox x        => collectVar x
-  | Expr.lit v          => skip
+  | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
   | Expr.isTaggedPtr x  => collectVar x
 
@@ -125,7 +125,7 @@ instance : AndThen Collector where
 
 private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
-  | irrelevant => skip
+  | _          => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun bv fv => as.foldl (fun fv a => f a bv fv) fv
@@ -145,7 +145,7 @@ private def collectExpr : Expr → Collector
   | Expr.ap x ys        => collectVar x >> collectArgs ys
   | Expr.box _ x        => collectVar x
   | Expr.unbox x        => collectVar x
-  | Expr.lit v          => skip
+  | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
   | Expr.isTaggedPtr x  => collectVar x
 
@@ -206,13 +206,13 @@ def visitExpr (w : Index) : Expr → Bool
   | Expr.ap x ys        => visitVar w x || visitArgs w ys
   | Expr.box _ x        => visitVar w x
   | Expr.unbox x        => visitVar w x
-  | Expr.lit v          => false
+  | Expr.lit _          => false
   | Expr.isShared x     => visitVar w x
   | Expr.isTaggedPtr x  => visitVar w x
 
 partial def visitFnBody (w : Index) : FnBody → Bool
-  | FnBody.vdecl x _ v b    => visitExpr w v || visitFnBody w b
-  | FnBody.jdecl j ys v b   => visitFnBody w v || visitFnBody w b
+  | FnBody.vdecl _ _ v b    => visitExpr w v || visitFnBody w b
+  | FnBody.jdecl _ _  v b   => visitFnBody w v || visitFnBody w b
   | FnBody.set x _ y b      => visitVar w x || visitArg w y || visitFnBody w b
   | FnBody.uset x _ y b     => visitVar w x || visitVar w y || visitFnBody w b
   | FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody w b
diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean
index 363045c21e..d83ff85765 100644
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@@ -43,8 +43,8 @@ abbrev visitArgs (w : Index) (as : Array Arg) : M Bool := pure (HasIndex.visitAr
 abbrev visitExpr (w : Index) (e : Expr) : M Bool := pure (HasIndex.visitExpr w e)
 
 partial def visitFnBody (w : Index) : FnBody → M Bool
-  | FnBody.vdecl x _ v b    => visitExpr w v <||> visitFnBody w b
-  | FnBody.jdecl j ys v b   => visitFnBody w v <||> visitFnBody w b
+  | FnBody.vdecl _ _ v b    => visitExpr w v <||> visitFnBody w b
+  | FnBody.jdecl _ _  v b   => visitFnBody w v <||> visitFnBody w b
   | FnBody.set x _ y b      => visitVar w x <||> visitArg w y <||> visitFnBody w b
   | FnBody.uset x _ y b     => visitVar w x <||> visitVar w y <||> visitFnBody w b
   | FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody w b
@@ -96,7 +96,7 @@ abbrev Collector := LiveVarSet → LiveVarSet
 
 private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
-  | irrelevant => skip
+  | _          => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun s =>
   as.foldl (fun s a => f a s) s
@@ -130,7 +130,7 @@ def collectExpr : Expr → Collector
   | Expr.ap x ys        => collectVar x ∘ collectArgs ys
   | Expr.box _ x        => collectVar x
   | Expr.unbox x        => collectVar x
-  | Expr.lit v          => skip
+  | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
   | Expr.isTaggedPtr x  => collectVar x
 
@@ -148,9 +148,9 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector
   | FnBody.dec x _ _ _ b,    m => collectVar x ∘ collectFnBody b m
   | FnBody.del x b,          m => collectVar x ∘ collectFnBody b m
   | FnBody.mdata _ b,        m => collectFnBody b m
-  | FnBody.ret x,            m => collectArg x
+  | FnBody.ret x,            _ => collectArg x
   | FnBody.case _ x _ alts,  m => collectVar x ∘ collectArray alts (fun alt => collectFnBody alt.body m)
-  | FnBody.unreachable,      m => skip
+  | FnBody.unreachable,      _ => skip
   | FnBody.jmp j xs,         m => collectJP m j ∘ collectArgs xs
 
 def updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) : JPLiveVarMap :=
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index 4f00063cfb..52e032ab61 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -69,7 +69,7 @@ def normExpr : Expr → M Expr
   | Expr.unbox x,        m => Expr.unbox (normVar x m)
   | Expr.isShared x,     m => Expr.isShared (normVar x m)
   | Expr.isTaggedPtr x,  m => Expr.isTaggedPtr (normVar x m)
-  | e@(Expr.lit v),      m =>  e
+  | e@(Expr.lit _),      _ =>  e
 
 abbrev N := ReaderT IndexRenaming (StateM Nat)
 
@@ -148,7 +148,7 @@ def mapExpr (f : VarId → VarId) : Expr → Expr
   | Expr.unbox x        => Expr.unbox (f x)
   | Expr.isShared x     => Expr.isShared (f x)
   | Expr.isTaggedPtr x  => Expr.isTaggedPtr (f x)
-  | e@(Expr.lit v)      =>  e
+  | e@(Expr.lit _)      =>  e
 
 partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody
   | FnBody.vdecl x t v b         => FnBody.vdecl x t (mapExpr f v) (mapFnBody f b)
diff --git a/src/Lean/Compiler/IR/PushProj.lean b/src/Lean/Compiler/IR/PushProj.lean
index 3079a13d2a..955f7e43cb 100644
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@@ -16,7 +16,7 @@ partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array Inde
     let bs   := bs.pop
     let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
     let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)
-    let push (x : VarId) (t : IRType) (v : Expr) :=
+    let push (x : VarId) (_ : IRType) (_ : Expr) :=
         if !ctxF.contains x.idx then
           let alts := alts.mapIdx fun i alt => alt.modifyBody fun b' =>
              if (altsF.get! i).contains x.idx then b.setBody b'
@@ -46,7 +46,7 @@ partial def FnBody.pushProj (b : FnBody) : FnBody :=
     let alts       := alts.map fun alt => alt.modifyBody pushProj
     let term       := FnBody.case tid x xType alts
     reshape bs term
-  | other => reshape bs term
+  | _     => reshape bs term
 
 /-- Push projections inside `case` branches. -/
 def Decl.pushProj (d : Decl) : Decl :=
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index b3017c56ba..1b274311ca 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -139,7 +139,7 @@ xs.size.fold (init := b) fun i b =>
     else b
 
 private def addIncBeforeConsumeAll (ctx : Context) (xs : Array Arg) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
-  addIncBeforeAux ctx xs (fun i => true) b liveVarsAfter
+  addIncBeforeAux ctx xs (fun _ => true) b liveVarsAfter
 
 /- Add `dec` instructions for parameters that are references, are not alive in `b`, and are not borrow.
    That is, we must make sure these parameters are consumed. -/
@@ -148,21 +148,21 @@ private def addDecForDeadParams (ctx : Context) (ps : Array Param) (b : FnBody)
     if !p.borrow && p.ty.isObj && !bLiveVars.contains p.x then addDec ctx p.x b else b
 
 private def isPersistent : Expr → Bool
-  | Expr.fap c xs => xs.isEmpty -- all global constants are persistent objects
+  | Expr.fap _ xs => xs.isEmpty -- all global constants are persistent objects
   | _             => false
 
 /- We do not need to consume the projection of a variable that is not consumed -/
 private def consumeExpr (m : VarMap) : Expr → Bool
-  | Expr.proj i x   => match m.find? x with
+  | Expr.proj _ x   => match m.find? x with
     | some info => info.consume
     | none      => true
-  | other => true
+  | _     => true
 
 /- Return true iff `v` at runtime is a scalar value stored in a tagged pointer.
    We do not need RC operations for this kind of value. -/
 private def isScalarBoxedInTaggedPtr (v : Expr) : Bool :=
   match v with
-  | Expr.ctor c ys          => c.size == 0 && c.ssize == 0 && c.usize == 0
+  | Expr.ctor c _           => c.size == 0 && c.ssize == 0 && c.usize == 0
   | Expr.lit (LitVal.num n) => n ≤ maxSmallNat
   | _ => false
 
@@ -198,7 +198,7 @@ private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b
       let ysx := ys.push (Arg.var x) -- TODO: avoid temporary array allocation
       addIncBeforeConsumeAll ctx ysx (FnBody.vdecl z t v b) bLiveVars
     | (Expr.unbox x)         => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
-    | other                  => FnBody.vdecl z t v b  -- Expr.reset, Expr.box, Expr.lit are handled here
+    | _                      => FnBody.vdecl z t v b  -- Expr.reset, Expr.box, Expr.lit are handled here
   let liveVars := updateLiveVars v bLiveVars
   let liveVars := liveVars.erase z
   (b, liveVars)
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index 36c8a4ad29..c869f121ee 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -63,7 +63,7 @@ partial def FnBody.simpCase (b : FnBody) : FnBody :=
   | FnBody.case tid x xType alts =>
     let alts := alts.map fun alt => alt.modifyBody simpCase;
     reshape bs (mkSimpCase tid x xType alts)
-  | other => reshape bs term
+  | _     => reshape bs term
 
 /-- Simplify `case`
   - Remove unreachable branches.
diff --git a/src/Lean/Compiler/IR/Sorry.lean b/src/Lean/Compiler/IR/Sorry.lean
index 0536b07d74..9d702872af 100644
--- a/src/Lean/Compiler/IR/Sorry.lean
+++ b/src/Lean/Compiler/IR/Sorry.lean
@@ -70,7 +70,7 @@ def updateSorryDep (decls : Array Decl) : CompilerM (Array Decl) := do
   let (_, s) ← Sorry.collect decls |>.run {}
   return decls.map fun decl =>
     match decl with
-    | Decl.fdecl f xs t b info =>
+    | Decl.fdecl f xs t b _    =>
       match s.localSorryMap.find? f with
       | some g => Decl.fdecl f xs t b { info with sorryDep? := some g }
       | _ => decl
diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean
index 975a2877be..3c349f55c2 100644
--- a/src/Lean/Compiler/NameMangling.lean
+++ b/src/Lean/Compiler/NameMangling.lean
@@ -8,7 +8,7 @@ import Lean.Data.Name
 namespace String
 
 private def mangleAux : Nat → String.Iterator → String → String
-  | 0,   it, r => r
+  | 0,   _,  r => r
   | i+1, it, r =>
     let c := it.curr
     if c.isAlpha || c.isDigit then
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index bacc0b83f4..56b466597e 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -229,7 +229,7 @@ def getObjValD (j : Json) (k : String) : Json :=
 
 def setObjVal! : Json → String → Json → Json
   | obj kvs, k, v => obj <| kvs.insert compare k v
-  | j      , _, _ => panic! "Json.setObjVal!: not an object: {j}"
+  | _      , _, _ => panic! "Json.setObjVal!: not an object: {j}"
 
 inductive Structured where
   | arr (elems : Array Json)
diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
index 13811eff58..78a976edba 100644
--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -168,7 +168,7 @@ partial def objectCore (anyCore : Unit → Parsec Json) : Parsec (RBNode String
 
 -- takes a unit parameter so that
 -- we can use the equation compiler and recursion
-partial def anyCore (u : Unit) : Parsec Json := do
+partial def anyCore (_ : Unit) : Parsec Json := do
   let c ← peek!
   if c = '[' then
     skip; ws
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 3c26188457..090c068968 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -27,7 +27,7 @@ instance : OfNat RequestID n := ⟨RequestID.num n⟩
 
 instance : ToString RequestID where
   toString
-  | RequestID.str s => s!"\"s\""
+  | RequestID.str _ => s!"\"s\""
   | RequestID.num n => toString n
   | RequestID.null => "null"
 
diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean
index 48c39a6092..07a46199ae 100644
--- a/src/Lean/Data/KVMap.lean
+++ b/src/Lean/Data/KVMap.lean
@@ -73,7 +73,7 @@ def size (m : KVMap) : Nat :=
   m.entries.length
 
 def findCore : List (Name × DataValue) → Name → Option DataValue
-  | [],       k' => none
+  | [],       _  => none
   | (k,v)::m, k' => if k == k' then some v else findCore m k'
 
 def find : KVMap → Name → Option DataValue
@@ -148,7 +148,7 @@ instance : ForIn m KVMap (Name × DataValue) where
   forIn := KVMap.forIn
 
 def subsetAux : List (Name × DataValue) → KVMap → Bool
-  | [],          m₂ => true
+  | [],          _  => true
   | (k, v₁)::m₁, m₂ =>
     match m₂.find k with
     | some v₂ => v₁ == v₂ && subsetAux m₁ m₂
@@ -167,13 +167,13 @@ class Value (α : Type) where
   toDataValue  : α → DataValue
   ofDataValue? : DataValue → Option α
 
-@[inline] def get? {α : Type} [s : Value α] (m : KVMap) (k : Name) : Option α :=
+@[inline] def get? {α : Type} [_ : Value α] (m : KVMap) (k : Name) : Option α :=
   m.find k |>.bind Value.ofDataValue?
 
-@[inline] def get {α : Type} [s : Value α] (m : KVMap) (k : Name) (defVal : α) : α :=
+@[inline] def get {α : Type} [_ : Value α] (m : KVMap) (k : Name) (defVal : α) : α :=
   m.get? k |>.getD defVal
 
-@[inline] def set {α : Type} [s : Value α] (m : KVMap) (k : Name) (v : α) : KVMap :=
+@[inline] def set {α : Type} [_ : Value α] (m : KVMap) (k : Name) (v : α) : KVMap :=
   m.insert k (Value.toDataValue v)
 
 instance : Value DataValue where
diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean
index 9684dc52fc..3db9403a80 100644
--- a/src/Lean/Data/Lsp/Extra.lean
+++ b/src/Lean/Data/Lsp/Extra.lean
@@ -30,10 +30,10 @@ structure WaitForDiagnosticsParams where
 structure WaitForDiagnostics
 
 instance : FromJson WaitForDiagnostics :=
-  ⟨fun j => pure WaitForDiagnostics.mk⟩
+  ⟨fun _ => pure WaitForDiagnostics.mk⟩
 
 instance : ToJson WaitForDiagnostics :=
-  ⟨fun o => mkObj []⟩
+  ⟨fun _ => mkObj []⟩
 
 inductive LeanFileProgressKind
   | processing | fatalError
diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean
index 334e451bca..29325d1a79 100644
--- a/src/Lean/Data/Lsp/Ipc.lean
+++ b/src/Lean/Data/Lsp/Ipc.lean
@@ -61,7 +61,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
     | Message.response id _ =>
       if id == waitForDiagnosticsId then return []
       else loop
-    | Message.responseError id code msg _ =>
+    | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
         throw $ userError s!"Waiting for diagnostics failed: {msg}"
       else loop
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index 80c18e6c9c..8f263ab1c0 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -28,7 +28,7 @@ def utf16Length (s : String) : Nat :=
   s.foldr (fun c acc => csize16 c + acc) 0
 
 private def codepointPosToUtf16PosFromAux (s : String) : Nat → Pos → Nat → Nat
-  | 0,    utf8pos, utf16pos => utf16pos
+  | 0,    _,       utf16pos => utf16pos
   | cp+1, utf8pos, utf16pos => codepointPosToUtf16PosFromAux s cp (s.next utf8pos) (utf16pos + csize16 (s.get utf8pos))
 
 /-- Computes the UTF-16 offset of the `n`-th Unicode codepoint
@@ -41,7 +41,7 @@ def codepointPosToUtf16Pos (s : String) (pos : Nat) : Nat :=
   codepointPosToUtf16PosFrom s pos 0
 
 private partial def utf16PosToCodepointPosFromAux (s : String) : Nat → Pos → Nat → Nat
-  | 0,        utf8pos, cp => cp
+  | 0,        _,       cp => cp
   | utf16pos, utf8pos, cp => utf16PosToCodepointPosFromAux s (utf16pos - csize16 (s.get utf8pos)) (s.next utf8pos) (cp + 1)
 
 /-- Computes the position of the Unicode codepoint at UTF-16 offset
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 353c4bf3d7..a7a996eeb1 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -18,8 +18,8 @@ namespace Name
 
 def getPrefix : Name → Name
   | anonymous => anonymous
-  | str p s _ => p
-  | num p s _ => p
+  | str p _ _ => p
+  | num p _ _ => p
 
 def getString! : Name → String
   | str _ s _ => s
@@ -31,9 +31,9 @@ def getNumParts : Name → Nat
   | num p _ _ => getNumParts p + 1
 
 def updatePrefix : Name → Name → Name
-  | anonymous, newP => anonymous
-  | str p s _, newP => Name.mkStr newP s
-  | num p s _, newP => Name.mkNum newP s
+  | anonymous, _    => anonymous
+  | str _ s _, newP => Name.mkStr newP s
+  | num _ s _, newP => Name.mkNum newP s
 
 def components' : Name → List Name
   | anonymous => []
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 48a76269b1..3a65a921e8 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -65,17 +65,17 @@ def setOptionFromString (opts : Options) (entry : String) : IO Options := do
   let key := Name.mkSimple key
   let defValue ← getOptionDefaulValue key
   match defValue with
-  | DataValue.ofString v => pure $ opts.setString key val
-  | DataValue.ofBool v   =>
+  | DataValue.ofString _ => pure $ opts.setString key val
+  | DataValue.ofBool _   =>
     if key == `true then pure $ opts.setBool key true
     else if key == `false then pure $ opts.setBool key false
     else throw $ IO.userError s!"invalid Bool option value '{val}'"
-  | DataValue.ofName v   => pure $ opts.setName key val.toName
-  | DataValue.ofNat v    =>
+  | DataValue.ofName _   => pure $ opts.setName key val.toName
+  | DataValue.ofNat _    =>
     match val.toNat? with
     | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
     | some v => pure $ opts.setNat key v
-  | DataValue.ofInt v    =>
+  | DataValue.ofInt _    =>
     match val.toInt? with
     | none   => throw (IO.userError s!"invalid Int option value '{val}'")
     | some v => pure $ opts.setInt key v
diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean
index 579ea17297..2ad20bab33 100644
--- a/src/Lean/Data/PrefixTree.lean
+++ b/src/Lean/Data/PrefixTree.lean
@@ -29,7 +29,7 @@ partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k
       let t := insertEmpty ks
       PrefixTreeNode.Node none (RBNode.singleton k t)
   let rec loop
-    | PrefixTreeNode.Node v m, [] =>
+    | PrefixTreeNode.Node _ m, [] =>
       PrefixTreeNode.Node (some val) m -- overrides old value
     | PrefixTreeNode.Node v m, k :: ks =>
       let t := match RBNode.find cmp m k with
@@ -41,8 +41,8 @@ partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k
 @[specialize]
 partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β :=
   let rec loop
-    | PrefixTreeNode.Node val m, [] => val
-    | PrefixTreeNode.Node val m, k :: ks =>
+    | PrefixTreeNode.Node val _, [] => val
+    | PrefixTreeNode.Node _   m, k :: ks =>
       match RBNode.find cmp m k with
       | none   => none
       | some t => loop t ks
diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean
index 9f62b47311..776d61f020 100644
--- a/src/Lean/Data/Trie.lean
+++ b/src/Lean/Data/Trie.lean
@@ -83,7 +83,7 @@ where
 
 private def updtAcc (v : Option α) (i : String.Pos) (acc : String.Pos × Option α) : String.Pos × Option α :=
   match v, acc with
-  | some v, (j, w) => (i, some v)  -- we pattern match on `acc` to enable memory reuse
+  | some v, (_, _) => (i, some v)  -- we pattern match on `acc` to enable memory reuse
   | none,   acc    => acc
 
 partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos × Option α :=
diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index d1c0eba660..083644151c 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -356,9 +356,9 @@ def toConstantVal : ConstantInfo → ConstantVal
 def isUnsafe : ConstantInfo → Bool
   | defnInfo   v => v.safety == DefinitionSafety.unsafe
   | axiomInfo  v => v.isUnsafe
-  | thmInfo    v => false
+  | thmInfo    _ => false
   | opaqueInfo v => v.isUnsafe
-  | quotInfo   v => false
+  | quotInfo   _ => false
   | inductInfo v => v.isUnsafe
   | ctorInfo   v => v.isUnsafe
   | recInfo    v => v.isUnsafe
@@ -381,8 +381,8 @@ def value? : ConstantInfo → Option Expr
   | _                         => none
 
 def hasValue : ConstantInfo → Bool
-  | defnInfo {value := r, ..} => true
-  | thmInfo  {value := r, ..} => true
+  | defnInfo {value := _, ..} => true
+  | thmInfo  {value := _, ..} => true
   | _                         => false
 
 def value! : ConstantInfo → Expr
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 4f64048e77..72c2b9aadf 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -466,7 +466,7 @@ mutual
 
   /- Elaborate function application arguments. -/
   partial def main : M Expr := do
-    let s ← get
+    let _ ← get
     let fType ← normalizeFunType
     if fType.isForall then
       let binderName := fType.bindingName!
@@ -614,7 +614,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       throwUnknownConstant (e.constName! ++ suffix)
     else
       throwInvalidFieldNotation e eType
-  | _, LVal.getOp _ idx => throwInvalidFieldNotation e eType
+  | _, LVal.getOp _ _   => throwInvalidFieldNotation e eType
   | _, _ => throwInvalidFieldNotation e eType
 
 /- whnfCore + implicit consumption.
@@ -622,7 +622,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
 private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × Expr) := do
   let eType ← whnfCore eType
   match eType with
-  | Expr.forallE n d b c =>
+  | Expr.forallE _ d b c =>
     if c.binderInfo.isImplicit || (hasArgs && c.binderInfo.isStrictImplicit) then
       let mvar ← mkFreshExprMVar d
       registerMVarErrorHoleInfo mvar.mvarId! stx
@@ -883,7 +883,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@$t:term) =>
+    | `($id:ident@$_:term) =>
       throwError "unexpected occurrence of named pattern"
     | `($id:ident) => do
       elabAppFnId id [] lvals namedArgs args expectedType? explicit ellipsis overloaded acc
@@ -894,7 +894,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$id:ident.{$us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
-    | `(@$t)     => throwUnsupportedSyntax -- invalid occurrence of `@`
+    | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
     | `(.$id:ident) =>
         let fConst ← mkConst (← resolveDotName id expectedType?)
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index c157d456d4..8961155231 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -295,7 +295,7 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
         let ident ← mkFreshIdent binder
         let type := binder
         loop body (i+1) (newBinders.push <| mkExplicitBinder ident type)
-      | Syntax.node _ ``Lean.Parser.Term.paren args =>
+      | Syntax.node _ ``Lean.Parser.Term.paren _    =>
         -- `(` (termParser >> parenSpecial)? `)`
         -- parenSpecial := (tupleTail <|> typeAscription)?
         let binderBody := binder[1]
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 71c1c197dd..71a6b1726b 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -46,7 +46,7 @@ def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α
   pure a
 
 private def popScopes (numScopes : Nat) : CommandElabM Unit :=
-  for i in [0:numScopes] do
+  for _ in [0:numScopes] do
     popScope
 
 private def checkAnonymousScope : List Scope → Bool
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index b8e29ab36d..62d4f1f4d0 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -20,7 +20,7 @@ private def ensureValidNamespace (name : Name) : MacroM Unit := do
     if s == "_root_" then
       Macro.throwError s!"invalid namespace '{name}', '_root_' is a reserved namespace"
     ensureValidNamespace p
-  | Name.num p .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
+  | Name.num _ .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
   | Name.anonymous => pure ()
 
 /- Auxiliary function for `expandDeclNamespace?` -/
@@ -28,7 +28,7 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
   let (id, optUnivDeclStx) := expandDeclIdCore declId
   let scpView := extractMacroScopes id
   match scpView.name with
-  | Name.str Name.anonymous s _ => return none
+  | Name.str Name.anonymous _ _ => return none
   | Name.str pre s _            =>
     ensureValidNamespace pre
     let nameNew := { scpView with name := Name.mkSimple s }.review
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 8b1da7aeef..fac0075094 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -22,7 +22,7 @@ where
   mkElseAlt : TermElabM Syntax := do
     let mut patterns := #[]
     -- add `_` pattern for indices
-    for i in [:indVal.numIndices] do
+    for _ in [:indVal.numIndices] do
       patterns := patterns.push (← `(_))
     patterns := patterns.push (← `(_))
     patterns := patterns.push (← `(_))
@@ -37,13 +37,13 @@ where
         let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
         let mut patterns := #[]
         -- add `_` pattern for indices
-        for i in [:indVal.numIndices] do
+        for _ in [:indVal.numIndices] do
           patterns := patterns.push (← `(_))
         let mut ctorArgs1 := #[]
         let mut ctorArgs2 := #[]
         let mut rhs ← `(true)
         -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.numParams] do
+        for _ in [:indVal.numParams] do
           ctorArgs1 := ctorArgs1.push (← `(_))
           ctorArgs2 := ctorArgs2.push (← `(_))
         for i in [:ctorInfo.numFields] do
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 8949bf609d..d10fed3f2c 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -45,7 +45,7 @@ where
       for ctorName₂ in indVal.ctors do
         let mut patterns := #[]
         -- add `_` pattern for indices
-        for i in [:indVal.numIndices] do
+        for _ in [:indVal.numIndices] do
           patterns := patterns.push (← `(_))
         if ctorName₁ == ctorName₂ then
           let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
@@ -54,7 +54,7 @@ where
             let mut ctorArgs1 := #[]
             let mut ctorArgs2 := #[]
             -- add `_` for inductive parameters, they are inaccessible
-            for i in [:indVal.numParams] do
+            for _ in [:indVal.numParams] do
               ctorArgs1 := ctorArgs1.push (← `(_))
               ctorArgs2 := ctorArgs2.push (← `(_))
             let mut todo := #[]
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 98090af69f..00640796b0 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -79,11 +79,11 @@ where
     forallTelescopeReducing ctorInfo.type fun xs type => do
       let mut patterns := #[]
       -- add `_` pattern for indices
-      for i in [:indVal.numIndices] do
+      for _ in [:indVal.numIndices] do
         patterns := patterns.push (← `(_))
       let mut ctorArgs := #[]
       -- add `_` for inductive parameters, they are inaccessible
-      for i in [:indVal.numParams] do
+      for _ in [:indVal.numParams] do
         ctorArgs := ctorArgs.push (← `(_))
       -- bound constructor arguments and their types
       let mut binders := #[]
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index 6a60634ad6..4eb37b8710 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -31,12 +31,12 @@ where
         let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
         let mut patterns := #[]
         -- add `_` pattern for indices
-        for i in [:indVal.numIndices] do
+        for _ in [:indVal.numIndices] do
           patterns := patterns.push (← `(_))
         let mut ctorArgs := #[]
         let mut rhs ← `($(quote ctorIdx))
         -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.numParams] do
+        for _ in [:indVal.numParams] do
           ctorArgs := ctorArgs.push (← `(_))
         for i in [:ctorInfo.numFields] do
           let x := xs[indVal.numParams + i]
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index 75ed7dd73e..b3f8e5d80d 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -24,7 +24,7 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name
     return false
 where
   addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
-    | [], i, map    => k map
+    | [], _, map    => k map
     | x::xs, i, map =>
       try
         let instType ← mkAppM `Inhabited #[x]
@@ -73,9 +73,9 @@ where
         binders := binders.push binder
     let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*))
     let mut ctorArgs := #[]
-    for i in [:ctorVal.numParams] do
+    for _ in [:ctorVal.numParams] do
       ctorArgs := ctorArgs.push (← `(_))
-    for i in [:ctorVal.numFields] do
+    for _ in [:ctorVal.numFields] do
       ctorArgs := ctorArgs.push (← ``(Inhabited.default))
     let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs:ident*⟩)
     `(instance $binders:explicitBinder* : $type := $val)
diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index 02637c6cab..548bafff11 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -27,14 +27,14 @@ where
         let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
         let mut indPatterns := #[]
         -- add `_` pattern for indices
-        for i in [:indVal.numIndices] do
+        for _ in [:indVal.numIndices] do
           indPatterns := indPatterns.push (← `(_))
         let mut ctorArgs1 := #[]
         let mut ctorArgs2 := #[]
         -- construct RHS top-down as continuation over the remaining comparison
         let mut rhsCont : Syntax → TermElabM Syntax := fun rhs => pure rhs
         -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.numParams] do
+        for _ in [:indVal.numParams] do
           ctorArgs1 := ctorArgs1.push (← `(_))
           ctorArgs2 := ctorArgs2.push (← `(_))
         for i in [:ctorInfo.numFields] do
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 5e59d6a3af..835b1719a9 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -56,13 +56,13 @@ where
       let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
         let mut patterns := #[]
         -- add `_` pattern for indices
-        for i in [:indVal.numIndices] do
+        for _ in [:indVal.numIndices] do
           patterns := patterns.push (← `(_))
         let mut ctorArgs := #[]
         let mut rhs := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
         -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.numParams] do
+        for _ in [:indVal.numParams] do
           ctorArgs := ctorArgs.push (← `(_))
         for i in [:ctorInfo.numFields] do
           let x := xs[indVal.numParams + i]
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index f5d07054af..d81e57f9f6 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -134,7 +134,7 @@ def mkHeader (ctx : Context) (className : Name) (arity : Nat) (indVal : Inductiv
   let binders       ← mkImplicitBinders argNames
   let targetType    ← mkInductiveApp indVal argNames
   let mut targetNames := #[]
-  for i in [:arity] do
+  for _ in [:arity] do
     targetNames := targetNames.push (← mkFreshUserName `x)
   let binders      := binders ++ (← mkInstImplicitBinders className indVal argNames)
   let binders      := binders ++ (← targetNames.mapM fun targetName => `(explicitBinderF| ($(mkIdent targetName) : $targetType)))
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index f9553235d7..c8f1632d63 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -222,7 +222,7 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | Code.«break» _              => m!"break {us}"
     | Code.«continue» _           => m!"continue {us}"
     | Code.«return» _ v           => m!"return {v} {us}"
-    | Code.«match» _ _ ds t alts  =>
+    | Code.«match» _ _ ds _ alts  =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
   loop codeBlock.code
@@ -241,7 +241,7 @@ partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool :=
   loop c
 
 def hasExitPoint (c : Code) : Bool :=
-  hasExitPointPred c fun c => true
+  hasExitPointPred c fun _ => true
 
 def hasReturn (c : Code) : Bool :=
   hasExitPointPred c fun
@@ -669,7 +669,7 @@ def mkSingletonDoSeq (doElem : Syntax) : Syntax :=
 /-
   If the given syntax is a `doIf`, return an equivalente `doIf` that has an `else` but no `else if`s or `if let`s.  -/
 private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx with
-  | `(doElem|if $p:doIfProp then $t else $e) => pure none
+  | `(doElem|if $_:doIfProp then $_ else $_) => pure none
   | `(doElem|if%$i $cond:doIfCond then $t $[else if%$is $conds:doIfCond then $ts]* $[else $e?]?) => withRef stx do
     let mut e      := e?.getD (← `(doSeq|pure PUnit.unit))
     let mut eIsSeq := true
@@ -1162,7 +1162,7 @@ structure ToForInTermResult where
   uvars      : Array Var
   term       : Syntax
 
-def mkForInBody  (x : Syntax) (forInBody : CodeBlock) : M ToForInTermResult := do
+def mkForInBody  (_ : Syntax) (forInBody : CodeBlock) : M ToForInTermResult := do
   let ctx ← read
   let uvars := forInBody.uvars
   let uvars := varSetToArray uvars
@@ -1274,7 +1274,7 @@ mutual
       let doElem := decl[3]
       let k ← withNewMutableVars #[y] (isMutableLet doLetArrow) (doSeqToCode doElems)
       match isDoExpr? doElem with
-      | some action => return mkVarDeclCore #[y] doLetArrow k
+      | some _      => return mkVarDeclCore #[y] doLetArrow k
       | none =>
         checkLetArrowRHS doElem
         let c ← doSeqToCode [doElem]
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index edb8d9246b..ea64f6499c 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -39,7 +39,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           catch
             ex => tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
-        | LOption.some val =>
+        | 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)
@@ -64,7 +64,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           catch
             ex => tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
-        | LOption.some val =>
+        | 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)
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 90d107020d..33ea7bf85e 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -298,10 +298,10 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
   | ofTermInfo i           => some i.toElabInfo
   | ofCommandInfo i        => some i.toElabInfo
-  | ofMacroExpansionInfo i => none
-  | ofFieldInfo i          => none
-  | ofCompletionInfo i     => none
-  | ofCustomInfo i         => none
+  | ofMacroExpansionInfo _ => none
+  | ofFieldInfo _          => none
+  | ofCompletionInfo _     => none
+  | ofCustomInfo _         => none
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index a9bb5ad274..3ae271a107 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -539,7 +539,7 @@ where
   processInaccessible (e : Expr) : M Expr := do
     let e' ← erasePatternRefAnnotations e
     match e' with
-    | Expr.fvar fvarId _ =>
+    | Expr.fvar _      _ =>
       if (← isExplicitPatternVar e') then
         processVar e
       else
@@ -873,7 +873,7 @@ private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Arr
       let ys := ysFVarIds.map mkFVar
       let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
         let type ← mkForallFVars ys type
-        let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, d) => di.isFVar
+        let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, _) => di.isFVar
         let type := type.replaceFVars discrs' ds'
         mkForallFVars ds type
       if (← isTypeCorrect matchType') then
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index b564112915..14cfae6797 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -19,7 +19,7 @@ structure EqnInfoCore where
   deriving Inhabited
 
 partial def expand : Expr → Expr
-  | Expr.letE _ t v b _ => expand (b.instantiate1 v)
+  | Expr.letE _ _ v b _ => expand (b.instantiate1 v)
   | Expr.mdata _ b _    => expand b
   | e => e
 
diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
index 9f968200ca..3a2ef060c4 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
@@ -16,7 +16,7 @@ open Meta
 private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do
   let mut result := #[]
   let mut t := t
-  for i in [:arity - 1] do
+  for _ in [:arity - 1] do
     result := result.push (mkProj ``PSigma 0 t)
     t := mkProj ``PSigma 1 t
   result.push t
@@ -137,7 +137,7 @@ where
           | Expr.forallE n d b c =>
             withLocalDecl n c.binderInfo (← visit d) fun x => do
               mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
-          | Expr.letE n t v b c  =>
+          | Expr.letE n t v b _  =>
             withLetDecl n (← visit t) (← visit v) fun x => do
               mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
           | Expr.proj n i s .. => return mkProj n i (← visit s)
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 314046e017..0df39f1dfe 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -133,7 +133,7 @@ where
     let hole ← `(_)
     for preDef in preDefs, numArg in numArgs, argIdx in argCombination, i in [:preDefs.size] do
       let mut vars := #[var]
-      for i in [:numArg - argIdx - 1] do
+      for _ in [:numArg - argIdx - 1] do
         vars := vars.push hole
       -- TODO: improve this.
       -- The following trick allows a function `f` in a mutual block to invoke `g` appearing before it with the input argument.
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 9df3253259..4595f10d32 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -79,7 +79,7 @@ end ArrayStxBuilder
 
 -- Elaborate the content of a syntax quotation term
 private partial def quoteSyntax : Syntax → TermElabM Syntax
-  | Syntax.ident info rawVal val preresolved => do
+  | Syntax.ident _    rawVal val preresolved => do
     if !hygiene.get (← getOptions) then
       return ← `(Syntax.ident info $(quote rawVal) $(quote val) $(quote preresolved))
     -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
@@ -249,7 +249,7 @@ structure HeadInfo where
 
 /-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so. -/
 private def noOpMatchAdaptPats : HeadCheck → Alt → Alt
-  | shape k (some sz), (pats, rhs) => (List.replicate sz (Unhygienic.run `(_)) ++ pats, rhs)
+  | shape _ (some sz), (pats, rhs) => (List.replicate sz (Unhygienic.run `(_)) ++ pats, rhs)
   | slice p s,         (pats, rhs) => (List.replicate (p + 1 + s) (Unhygienic.run `(_)) ++ pats, rhs)
   | _,                 alt         => alt
 
@@ -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 `($f:ident $[ $args:ident]*) := rhs then
+    if let `($_:ident $[ $args:ident]*) := rhs then
       -- looks simple enough/created by this function, skip
       return (floatedLetDecls, (pats, rhs))
     withFreshMacroScope do
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index e3270464ec..e971b878b2 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -82,7 +82,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
 
 @[builtinQuotPrecheck ident] def precheckIdent : Precheck := fun stx =>
   match stx with
-  | Syntax.ident info rawVal val preresolved => do
+  | Syntax.ident _    _      val preresolved => do
     if !preresolved.isEmpty then
       return
     /- The precheck currently ignores field notation.
@@ -99,7 +99,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     let rs ← try resolveName stx val [] [] catch _ => pure []
     for (e, _) in rs do
       match e with
-      | Expr.fvar fvarId .. =>
+      | Expr.fvar _      .. =>
         if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then
           return
       | _ => pure ()
@@ -111,7 +111,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     precheck f
     for arg in args do
       match arg with
-      | `(argument| ($n := $e)) => precheck e
+      | `(argument| ($_ := $e)) => precheck e
       | `(argument| $e:term)    => precheck e
       | `(argument| ..)         => pure ()
       | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/RecAppSyntax.lean b/src/Lean/Elab/RecAppSyntax.lean
index ad742168b8..1d377a5a60 100644
--- a/src/Lean/Elab/RecAppSyntax.lean
+++ b/src/Lean/Elab/RecAppSyntax.lean
@@ -21,7 +21,7 @@ def mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr :=
 -/
 def getRecAppSyntax? (e : Expr) : Option Syntax :=
   match e with
-  | Expr.mdata d b _ =>
+  | Expr.mdata d _ _ =>
     match d.find recAppKey with
     | some (DataValue.ofSyntax stx) => some stx
     | _ => none
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 04e488df5f..51806f59a3 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -291,7 +291,7 @@ def formatField (formatStruct : Struct → Format) (field : Field Struct) : Form
     | FieldVal.default  => "<default>"
 
 partial def formatStruct : Struct → Format
-  | ⟨_, structName, _, fields, source⟩ =>
+  | ⟨_, _,          _, fields, source⟩ =>
     let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
     match source with
     | Source.none             => "{" ++ fieldsFmt ++ "}"
@@ -419,7 +419,7 @@ private def expandNumLitFields (s : Struct) : TermElabM Struct :=
 private def expandParentFields (s : Struct) : TermElabM Struct := do
   let env ← getEnv
   s.modifyFieldsM fun fields => fields.mapM fun field => match field with
-    | { lhs := FieldLHS.fieldName ref fieldName :: rest, .. } =>
+    | { lhs := FieldLHS.fieldName ref fieldName :: _,    .. } =>
       match findField? env s.structName fieldName with
       | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{s.structName}'"
       | some baseStructName =>
@@ -438,7 +438,7 @@ private abbrev FieldMap := HashMap Name Fields
 private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
   fields.foldlM (init := {}) fun fieldMap field =>
     match field.lhs with
-    | FieldLHS.fieldName _ fieldName :: rest =>
+    | FieldLHS.fieldName _ fieldName :: _    =>
       match fieldMap.find? fieldName with
       | some (prevField::restFields) =>
         if field.isSimple || prevField.isSimple then
@@ -574,7 +574,7 @@ private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array (
 
 private partial def getForallBody : Nat → Expr → Option Expr
   | i+1, Expr.forallE _ _ b _ => getForallBody i b
-  | i+1, _                    => none
+  | _+1, _                    => none
   | 0,   type                 => type
 
 private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit :=
@@ -838,7 +838,7 @@ partial def step (struct : Struct) : M Unit :=
               unless (← isExprMVarAssigned mvarId) do
                 let ctx ← read
                 if (← withRef field.ref <| tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then
-                  modify fun s => { s with progress := true }
+                  modify fun _ => { s with progress := true }
             | _ => pure ()
 
 partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do
@@ -849,7 +849,7 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M
     if d > hierarchyDepth then
       throwErrorAt field.ref "field '{getFieldName field}' is missing"
     else withReader (fun ctx => { ctx with maxDistance := d }) do
-      modify fun s => { s with progress := false }
+      modify fun _ => { s with progress := false }
       step struct
       if (← get).progress then do
         propagateLoop hierarchyDepth 0 struct
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index a8271c22b6..f252c774b3 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -747,7 +747,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
   let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
-  let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
+  let Expr.const parentStructName _  _ ← pure parentType.getAppFn | unreachable!
   let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
   withLocalDecl `self binfo structType fun source => do
     let declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 31dd341fd7..369fe73445 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -365,7 +365,7 @@ mutual
     pending TC problems become implicit parameters for the simp theorem.
   -/
   partial def synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := false) : TermElabM Unit := do
-    let rec loop (u : Unit) : TermElabM Unit := do
+    let rec loop (_ : Unit) : TermElabM Unit := do
       withRef (← getSomeSynthethicMVarsRef) <| withIncRecDepth do
         unless (← get).syntheticMVars.isEmpty do
           if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 5699c7ff14..3118c179f9 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -60,7 +60,7 @@ def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 
 def setGoals (mvarIds : List MVarId) : TacticM Unit :=
-  modify fun s => { s with goals := mvarIds }
+  modify fun _ => { s with goals := mvarIds }
 
 def pruneSolvedGoals : TacticM Unit := do
   let gs ← getGoals
@@ -177,7 +177,7 @@ mutual
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
     withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
-      | Syntax.node _ k args =>
+      | Syntax.node _ k _    =>
         if k == nullKind then
           -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
           stx.getArgs.forM evalTactic
@@ -256,7 +256,7 @@ instance {α} : OrElse (TacticM α) where
   orElse := Tactic.orElse
 
 instance : Alternative TacticM where
-  failure := fun {α} => throwError "failed"
+  failure := fun {_} => throwError "failed"
   orElse  := Tactic.orElse
 
 /-
@@ -284,7 +284,7 @@ def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
 
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (mvarId :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
-  modify fun s => { s with goals := mvarIds ++ mvarIds' }
+  modify fun _ => { s with goals := mvarIds ++ mvarIds' }
 
 /-- Return the first goal. -/
 def getMainGoal : TacticM MVarId := do
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index e3fb25a229..7e94f7c99f 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -70,9 +70,9 @@ inductive MVarErrorKind where
 
 instance : ToString MVarErrorKind where
   toString
-    | MVarErrorKind.implicitArg ctx => "implicitArg"
+    | MVarErrorKind.implicitArg _   => "implicitArg"
     | MVarErrorKind.hole            => "hole"
-    | MVarErrorKind.custom msg      => "custom"
+    | MVarErrorKind.custom _        => "custom"
 
 structure MVarErrorInfo where
   mvarId    : MVarId
@@ -1040,7 +1040,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
         (try
           elabFn.value stx expectedType?
         catch ex => match ex with
-          | Exception.error ref msg =>
+          | Exception.error _   _   =>
             if (← read).errToSorry then
               exceptionToSorry ex expectedType?
             else
@@ -1092,7 +1092,7 @@ instance : MonadMacroAdapter TermElabM where
 
 private def isExplicit (stx : Syntax) : Bool :=
   match stx with
-  | `(@$f) => true
+  | `(@$_) => true
   | _      => false
 
 private def isExplicitApp (stx : Syntax) : Bool :=
@@ -1115,22 +1115,22 @@ private def isHole (stx : Syntax) : Bool :=
   match stx with
   | `(_)          => true
   | `(? _)        => true
-  | `(? $x:ident) => true
+  | `(? $_:ident) => true
   | _             => false
 
 private def isTacticBlock (stx : Syntax) : Bool :=
   match stx with
-  | `(by $x:tacticSeq) => true
+  | `(by $_:tacticSeq) => true
   | _ => false
 
 private def isNoImplicitLambda (stx : Syntax) : Bool :=
   match stx with
-  | `(no_implicit_lambda% $x:term) => true
+  | `(no_implicit_lambda% $_:term) => true
   | _ => false
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($e : $type)) => true
+  | `(($_ : $type)) => true
   | _               => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
@@ -1541,7 +1541,7 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr
   `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
 def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   match ident with
-  | Syntax.ident info rawStr n preresolved =>
+  | Syntax.ident _    _      n preresolved =>
     let r ← resolveName ident n preresolved explicitLevels expectedType?
     r.mapM fun (c, fields) => do
       let ids := ident.identComponents (nFields? := fields.length)
@@ -1552,7 +1552,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
   match stx with
   | Syntax.ident _ _ val preresolved => do
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
-    let rs := rs.filter fun ⟨f, projs⟩ => projs.isEmpty
+    let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => return none
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 16b2a2f87d..a0a8ec22d5 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -203,7 +203,7 @@ partial def ensureExtensionsArraySize (env : Environment) : IO Environment := do
 where
   loop (i : Nat) (env : Environment) : IO Environment := do
     let envExtensions ← envExtensionsRef.get
-    if h : i < envExtensions.size then
+    if _ : i < envExtensions.size then
       let s ← envExtensions[i].mkInitial
       let env := { env with extensions := env.extensions.push s }
       loop (i + 1) env
@@ -592,7 +592,7 @@ where
   loop (i : Nat) (env : Environment) : IO Environment := do
     -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
     let pExtDescrs ← persistentEnvExtensionsRef.get
-    if h : i < pExtDescrs.size then
+    if _ : i < pExtDescrs.size then
       let extDescr := pExtDescrs[i]
       let s := extDescr.toEnvExtension.getState env
       let prevSize := (← persistentEnvExtensionsRef.get).size
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 44f2ca4a33..4148752a0a 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -558,12 +558,12 @@ def getForallBody : Expr → Expr
 function applications `f a₁ .. aₙ`, return `f`.
 Otherwise return the input expression. -/
 def getAppFn : Expr → Expr
-  | app f a _ => getAppFn f
+  | app f _ _ => getAppFn f
   | e         => e
 
 def getAppNumArgsAux : Expr → Nat → Nat
-  | app f a _, n => getAppNumArgsAux f (n+1)
-  | e,         n => n
+  | app f _ _, n => getAppNumArgsAux f (n+1)
+  | _,         n => n
 
 /-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`. -/
 def getAppNumArgs (e : Expr) : Nat :=
@@ -589,7 +589,7 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
 
 @[specialize] def withAppAux (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α
   | app f a _, as, i => withAppAux k f (as.set! i a) (i-1)
-  | f,         as, i => k f as
+  | f,         as, _ => k f as
 
 /-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/
 @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α :=
@@ -606,12 +606,12 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   withAppRevAux k e (Array.mkEmpty e.getAppNumArgs)
 
 def getRevArgD : Expr → Nat → Expr → Expr
-  | app f a _, 0,   _ => a
+  | app _ a _, 0,   _ => a
   | app f _ _, i+1, v => getRevArgD f i v
   | _,         _,   v => v
 
 def getRevArg! : Expr → Nat → Expr
-  | app f a _, 0   => a
+  | app _ a _, 0   => a
   | app f _ _, i+1 => getRevArg! f i
   | _,         _   => panic! "invalid index"
 
@@ -979,7 +979,7 @@ def isHeadBetaTarget (e : Expr) (useZeta := false) : Bool :=
 
 private def etaExpandedBody : Expr → Nat → Nat → Option Expr
   | app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none
-  | _,                  n+1, _ => none
+  | _,                  _+1, _ => none
   | f,                  0,   _ => if f.hasLooseBVars then none else some f
 
 private def etaExpandedAux : Expr → Nat → Option Expr
@@ -1046,8 +1046,8 @@ partial def consumeMDataAndTypeAnnotations (e : Expr) : Expr :=
     | Expr.letE _ t v b _    => visit t || visit v || visit b
     | Expr.app f a _         => visit f || visit a
     | Expr.proj _ _ e _      => visit e
-    | e@(Expr.fvar fvarId _) => p fvarId
-    | e                      => false
+    | _@(Expr.fvar fvarId _) => p fvarId
+    | _                      => false
   visit e
 
 def containsFVar (e : Expr) (fvarId : FVarId) : Bool :=
@@ -1171,9 +1171,9 @@ partial def eta (e : Expr) : Expr :=
   let rec @[specialize] visit (e : Expr) : Expr :=
     if !e.hasLevelParam then e
     else match e with
-    | lam n d b _     => e.updateLambdaE! (visit d) (visit b)
-    | forallE n d b _ => e.updateForallE! (visit d) (visit b)
-    | letE n t v b _  => e.updateLet! (visit t) (visit v) (visit b)
+    | lam _ d b _     => e.updateLambdaE! (visit d) (visit b)
+    | forallE _ d b _ => e.updateForallE! (visit d) (visit b)
+    | letE _ t v b _  => e.updateLet! (visit t) (visit v) (visit b)
     | app f a _       => e.updateApp! (visit f) (visit a)
     | proj _ _ s _    => e.updateProj! (visit s)
     | mdata _ b _     => e.updateMData! (visit b)
@@ -1272,7 +1272,7 @@ private def patternRefAnnotationKey := `_patWithRef
 -/
 def patternWithRef? (p : Expr) : Option (Syntax × Expr) :=
   match p with
-  | Expr.mdata d b _ =>
+  | Expr.mdata d _ _ =>
     match d.find patternRefAnnotationKey with
     | some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!)
     | _ => none
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 4c41fefb3e..537b541ea5 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -28,7 +28,7 @@ abbrev Key := Name
 `KeyedDeclsAttribute` definition.
 
  Important: `mkConst valueTypeName` and `γ` must be definitionally equal. -/
-structure Def (γ : Type) where
+structure Def (_ : Type) where
   builtinName   : Name := Name.anonymous  -- Builtin attribute name, if any (e.g., `builtinTermElab)
   name          : Name    -- Attribute name (e.g., `termElab)
   descr         : String  -- Attribute description
@@ -103,7 +103,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
   let ext : Extension γ ← registerScopedEnvExtension {
     name         := df.name
     mkInitial    := return mkStateOfTable (← tableRef.get)
-    ofOLeanEntry := fun s entry => do
+    ofOLeanEntry := fun _ entry => do
       let ctx ← read
       match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.declName with
       | Except.ok f     => return { toOLeanEntry := entry, value := f }
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 306f8c7e8f..f5f8763bb6 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -196,7 +196,7 @@ def isNeverZero : Level → Bool
   | mvar ..      => false
   | succ ..      => true
   | max l₁ l₂ _  => isNeverZero l₁ || isNeverZero l₂
-  | imax l₁ l₂ _ => isNeverZero l₂
+  | imax _  l₂ _ => isNeverZero l₂
 
 def ofNat : Nat → Level
   | 0   => levelZero
@@ -559,11 +559,11 @@ where
   go (u v : Level) : Bool :=
     u == v ||
     match u, v with
-    | u,            zero _       => true
+    | _,            zero _       => true
     | u,            max v₁ v₂ _  => go u v₁ && go u v₂
     | max u₁ u₂ _,  v            => go u₁ v || go u₂ v
     | u,            imax v₁ v₂ _ => go u v₁ && go u v₂
-    | imax u₁ u₂ _, v            => go u₂ v
+    | imax _  u₂ _, v            => go u₂ v
     | succ u _,     succ v _     => go u v
     | _, _ =>
       let v' := v.getLevelOffset
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index dc1e3f4f7f..1888b09cd2 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -171,8 +171,8 @@ def bracket (l : String) (f : MessageData) (r : String) : MessageData := group (
 def paren (f : MessageData) : MessageData := bracket "(" f ")"
 def sbracket (f : MessageData) : MessageData := bracket "[" f "]"
 def joinSep : List MessageData → MessageData → MessageData
-  | [],    sep => Format.nil
-  | [a],   sep => a
+  | [],    _   => Format.nil
+  | [a],   _   => a
   | a::as, sep => a ++ sep ++ joinSep as sep
 def ofList: List MessageData → MessageData
   | [] => "[]"
@@ -318,7 +318,7 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   match e with
   | unknownConstant env constName       => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'"
   | alreadyDeclared env constName       => mkCtx env {} opts m!"(kernel) constant has already been declared '{constName}'"
-  | declTypeMismatch env decl givenType =>
+  | declTypeMismatch _   decl givenType =>
     let process (n : Name) (expectedType : Expr) : MessageData :=
       m!"(kernel) declaration type mismatch, '{n}' has type{indentExpr givenType}\nbut it is expected to have type{indentExpr expectedType}";
     match decl with
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 1ee7cf4592..1704abe160 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -919,7 +919,7 @@ where
       finalize ()
     else
       match type with
-      | Expr.lam n d b c =>
+      | Expr.lam _ d b c =>
         let d     := d.instantiateRevRange j mvars.size mvars
         let mvar ← mkFreshExprMVar d
         let mvars := mvars.push mvar
@@ -1161,7 +1161,7 @@ def ppExpr (e : Expr) : MetaM Format := do
 instance : OrElse (MetaM α) := ⟨Meta.orElse⟩
 
 instance : Alternative MetaM where
-  failure := fun {α} => throwError "failed"
+  failure := fun {_} => throwError "failed"
   orElse  := Meta.orElse
 
 @[inline] private def orelseMergeErrorsImp (x y : MetaM α)
diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean
index 02473bb801..0ee8e05b77 100644
--- a/src/Lean/Meta/CasesOn.lean
+++ b/src/Lean/Meta/CasesOn.lean
@@ -89,9 +89,9 @@ where
     for alt in c.alts, numParams in c.altNumParams do
       auxType ← whnfD auxType
       match auxType with
-      | .forallE n d b _ =>
+      | .forallE _ d b _ =>
         let (altNew, refinedAt) ← forallBoundedTelescope d (some numParams) fun xs d => do
-          forallBoundedTelescope d (some 1) fun x d => do
+          forallBoundedTelescope d (some 1) fun x _ => do
             let alt := alt.beta xs
             let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
             if checkIfRefined then
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index e70f5d00e0..682c81bacf 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -18,7 +18,7 @@ private def ensureType (e : Expr) : MetaM Unit := do
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
   let lctx ← getLCtx
   match lctx.find? fvarId with
-  | some (LocalDecl.ldecl _ _ n t v _) => do
+  | some (LocalDecl.ldecl _ _ _ t v _) => do
     let vType ← inferType v
     throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
   | _ => unreachable!
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index f4db719e1c..ab2dfeb8ea 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -195,7 +195,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
   | Expr.app f a _       => return e.updateApp! (← collect f) (← collect a)
   | Expr.mdata _ b _     => return e.updateMData! (← collect b)
   | Expr.sort u _        => return e.updateSort! (← collectLevel u)
-  | Expr.const c us _    => return e.updateConst! (← us.mapM collectLevel)
+  | Expr.const _ us _    => return e.updateConst! (← us.mapM collectLevel)
   | Expr.mvar mvarId _   =>
     let mvarDecl ← getMVarDecl mvarId
     let type ← preprocess mvarDecl.type
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 1859b94391..c9ee301aa8 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -244,7 +244,7 @@ private def isBadKey (fn : Expr) : Bool :=
   | Expr.const .. => false
   | Expr.fvar ..  => false
   | Expr.proj ..  => false
-  | Expr.forallE _ d b _ => b.hasLooseBVars
+  | Expr.forallE _ _ b _ => b.hasLooseBVars
   | _ => true
 
 /--
@@ -550,7 +550,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
 where
   process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
     match skip, c with
-    | skip+1, Trie.node vs cs =>
+    | skip+1, Trie.node _  cs =>
       if cs.isEmpty then
         return result
       else
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 0dc5b84095..6733c50319 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -804,7 +804,7 @@ partial def check
     | Expr.fvar fvarId ..  =>
       if mvarDecl.lctx.contains fvarId then true
       else match lctx.find? fvarId with
-        | some (LocalDecl.ldecl (value := v) ..) => false -- need expensive CheckAssignment.check
+        | some (LocalDecl.ldecl (value := _) ..) => false -- need expensive CheckAssignment.check
         | _ =>
           if fvars.any fun x => x.fvarId! == fvarId then true
           else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 77c1510e17..67fd64916e 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -88,7 +88,7 @@ where
           mkForallFVars (xs.insertAt numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
-    forallTelescopeReducing indVal.type fun xs t => do
+    forallTelescopeReducing indVal.type fun xs _ => do
       mkForallFVars xs (← mkArrow (mkAppN (mkIndValConst indVal) xs) (mkSort levelZero))
 
   mkIndValConst (indVal : InductiveVal) : Expr :=
@@ -133,7 +133,7 @@ where
     else rebuild vars
 
   rebuild (vars : Variables) :=
-    vars.innerType.withApp fun f args => do
+    vars.innerType.withApp fun _ args => do
       let hApp :=
         mkAppN
           (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam)
@@ -194,7 +194,7 @@ where
       (domain : Expr)
       {α : Type} (k : Expr → MetaM α) : MetaM α := do
     forallTelescopeReducing domain fun xs t => do
-      t.withApp fun f args => do
+      t.withApp fun _ args => do
         let hApp := mkAppN binder xs
         let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp]
         let newDomain ← mkForallFVars xs t
@@ -299,7 +299,7 @@ where
         let ctorName := ctor.constName!.updatePrefix below.constName!
         let ctor := mkConst ctorName below.constLevels!
         let ctorInfo ← getConstInfoCtor ctorName
-        let (mvars, _, t) ← forallMetaTelescope ctorInfo.type
+        let (mvars, _, _) ← forallMetaTelescope ctorInfo.type
         let ctor := mkAppN ctor mvars
         apply m ctor
     return mss.foldr List.append []
@@ -325,7 +325,7 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
     value := ←proveBrecOn ctx indVal type }
 where
   mkType : MetaM Expr :=
-    forallTelescopeReducing ctx.headers[idx] fun xs t => do
+    forallTelescopeReducing ctx.headers[idx] fun xs _ => do
     let params := xs[:ctx.numParams]
     let motives := xs[ctx.numParams:ctx.numParams + ctx.motives.size].toArray
     let indices := xs[ctx.numParams + ctx.motives.size:]
@@ -343,7 +343,7 @@ where
       else mkFreshUserName "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
-      forallTelescopeReducing ih fun ys t => do
+      forallTelescopeReducing ih fun ys _ => do
         let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam
         let args := params ++ motives ++ ys
         let premise :=
@@ -359,7 +359,7 @@ 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 t => do
+  forallTelescopeReducing ctorInfo.type fun xs _ => do
   loop xs belowCtorInfo.type #[] 0 0
 
 where
@@ -425,7 +425,7 @@ partial def mkBelowMatcher
     let xs :=
       -- special case: if we had no free vars, i.e. there was a unit added and no we do have free vars, we get rid of the unit.
       match oldFVars.size, fvars.size with
-      | 0, n+1 => xs[1:]
+      | 0, _+1 => xs[1:]
       | _, _ => xs
     let t := t.replaceFVars xs[:oldFVars.size] fvars[:oldFVars.size]
     trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]}"
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 77f8144062..b8d7dd4a49 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -40,7 +40,7 @@ where
       | Expr.letE _ t v b _    => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
       | Expr.mdata _ b _       => return e.updateMData! (← visit b offset)
       | Expr.proj _ _ b _      => return e.updateProj! (← visit b offset)
-      | Expr.app f a _         =>
+      | Expr.app _ _ _         =>
         e.withAppRev fun f revArgs => do
         let fNew    ← visit f offset
         let revArgs ← revArgs.mapM (visit · offset)
@@ -305,7 +305,7 @@ partial def isProofQuick : Expr → MetaM LBool
   | Expr.lam _ _ b _      => isProofQuick b
   | Expr.letE _ _ _ b _   => isProofQuick b
   | Expr.proj _ _ _ _     => return LBool.undef
-  | Expr.forallE _ _ b _  => return LBool.false
+  | Expr.forallE _ _ _ _  => return LBool.false
   | Expr.mdata _ e _      => isProofQuick e
   | Expr.const c lvls _   => do let constType ← inferConstType c lvls; isArrowProposition constType 0
   | Expr.fvar fvarId _    => do let fvarType  ← inferFVarType fvarId;  isArrowProposition fvarType 0
@@ -328,7 +328,7 @@ def isProof (e : Expr) : MetaM Bool := do
    if `type` is of the form `A_1 -> ... -> A_n -> Sort _`.
    Remark: `type` can be a dependent arrow. -/
 private partial def isArrowType : Expr → Nat → MetaM LBool
-  | Expr.sort u _,        0   => return LBool.true
+  | Expr.sort _ _,        0   => return LBool.true
   | Expr.forallE _ _ _ _, 0   => return LBool.false
   | Expr.forallE _ _ b _, n+1 => isArrowType b n
   | Expr.letE _ _ _ b _,  n   => isArrowType b n
@@ -359,7 +359,7 @@ partial def isTypeQuick : Expr → MetaM LBool
   | Expr.lam _ _ _ _      => return LBool.false
   | Expr.letE _ _ _ b _   => isTypeQuick b
   | Expr.proj _ _ _ _     => return LBool.undef
-  | Expr.forallE _ _ b _  => return LBool.true
+  | Expr.forallE _ _ _ _  => return LBool.true
   | Expr.mdata _ e _      => isTypeQuick e
   | Expr.const c lvls _   => do let constType ← inferConstType c lvls; isArrowType constType 0
   | Expr.fvar fvarId _    => do let fvarType  ← inferFVarType fvarId;  isArrowType fvarType 0
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index 8de4794148..238920fa1f 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -37,7 +37,7 @@ partial def toMessageData : Pattern → MessageData
   | ctor ctorName _ _ pats => m!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
   | val e                  => e
   | arrayLit _ pats        => m!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
-  | as varId p h           => m!"{mkFVar varId}@{toMessageData p}"
+  | as varId p _           => m!"{mkFVar varId}@{toMessageData p}"
 
 partial def toExpr (p : Pattern) (annotate := false) : MetaM Expr :=
   visit p
@@ -220,7 +220,7 @@ partial def applyFVarSubst (s : FVarSubst) : Example → Example
   | ex           => ex
 
 partial def varsToUnderscore : Example → Example
-  | var x        => underscore
+  | var _        => underscore
   | ctor n exs   => ctor n $ exs.map varsToUnderscore
   | arrayLit exs => arrayLit $ exs.map varsToUnderscore
   | ex           => ex
diff --git a/src/Lean/Meta/Match/CaseArraySizes.lean b/src/Lean/Meta/Match/CaseArraySizes.lean
index d48ea921a1..9bfc2c79c6 100644
--- a/src/Lean/Meta/Match/CaseArraySizes.lean
+++ b/src/Lean/Meta/Match/CaseArraySizes.lean
@@ -60,7 +60,7 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
 def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
   withMVarContext mvarId do
     let a := mkFVar fvarId
-    let α ← getArrayArgType a
+    let _ ← getArrayArgType a
     let aSize ← mkAppM `Array.size #[a]
     let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize
     let (aSizeFVarId, mvarId) ← intro1 mvarId
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index 772e530947..cbe36f8298 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -81,7 +81,7 @@ structure CaseValuesSubgoal where
 -/
 def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) (substNewEqs := false) : MetaM (Array CaseValuesSubgoal) :=
   let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
-    | i, mvarId, [],    hs, subgoals => throwTacticEx `caseValues mvarId "list of values must not be empty"
+    | _, mvarId, [],    _,  _        => throwTacticEx `caseValues mvarId "list of values must not be empty"
     | i, mvarId, v::vs, hs, subgoals => do
       let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
       appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 860621edca..424b3a1a92 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -30,7 +30,7 @@ private partial def withEqs (lhs rhs : Array Expr) (discrInfos : Array DiscrInfo
   go 0 #[]
 where
   go (i : Nat) (hs : Array Expr) : MetaM α := do
-    if h : i < lhs.size then
+    if _ : i < lhs.size then
       if let some hName := discrInfos[i].hName? then
         withLocalDeclD hName (← mkEqHEq lhs[i] rhs[i]) fun h =>
           go (i+1) (hs.push h)
@@ -160,7 +160,7 @@ private def isNatValueTransition (p : Problem) : Bool :=
 private def processSkipInaccessible (p : Problem) : Problem :=
   match p.vars with
   | []      => unreachable!
-  | x :: xs =>
+  | _ :: xs =>
     let alts := p.alts.map fun alt => match alt.patterns with
       | Pattern.inaccessible _ :: ps => { alt with patterns := ps }
       | _       => unreachable!
@@ -182,7 +182,7 @@ private def processLeaf (p : Problem) : StateRefT State MetaM Unit := do
 private def processAsPattern (p : Problem) : MetaM Problem :=
   match p.vars with
   | []      => unreachable!
-  | x :: xs => withGoalOf p do
+  | x :: _  => withGoalOf p do
     let alts ← p.alts.mapM fun alt => do
       match alt.patterns with
       | Pattern.as fvarId p h :: ps =>
@@ -546,7 +546,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
     let sizes := collectArraySizes p
     let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
     subgoals.mapIdxM fun i subgoal => do
-      if h : i.val < sizes.size then
+      if _ : i.val < sizes.size then
         let size     := sizes.get! i
         let subst    := subgoal.subst
         let elems    := subgoal.elems.toList
@@ -628,7 +628,7 @@ private def moveToFront (p : Problem) (i : Nat) : Problem :=
   if i == 0 then
     p
   else if h : i < p.vars.length then
-    let x := p.vars.get ⟨i, h⟩
+    let _ := p.vars.get ⟨i, h⟩
     { p with
       vars := List.moveToFront p.vars i
       alts := p.alts.map fun alt => { alt with patterns := List.moveToFront alt.patterns i }
@@ -891,7 +891,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
       if let some idx := matcherInfo.uElimPos?
       then mkLevelParam matcherConst.levelParams.toArray[idx]
       else levelZero
-    forallBoundedTelescope matcherType (some matcherInfo.numDiscrs) fun discrs t => do
+    forallBoundedTelescope matcherType (some matcherInfo.numDiscrs) fun discrs _ => do
     mkForallFVars discrs (mkConst ``PUnit [u])
 
   let matcherType ← instantiateForall matcherType matcherApp.discrs
@@ -900,7 +900,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
     let ty ← inferType alt
     forallTelescope ty fun xs body => do
     let xs ← xs.filterM fun x => dependsOn body x.fvarId!
-    body.withApp fun f args => do
+    body.withApp fun _ args => do
     let ctx ← getLCtx
     let localDecls := xs.map ctx.getFVar!
     let patterns ← args.mapM Match.toPattern
@@ -915,7 +915,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
 def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) : MetaM α := do
   let some matcherInfo ← getMatcherInfo? matcherName | throwError "not a matcher: {matcherName}"
   let matcherConst ← getConstInfo matcherName
-  forallBoundedTelescope matcherConst.type (some matcherInfo.arity) fun xs t => do
+  forallBoundedTelescope matcherConst.type (some matcherInfo.arity) fun xs _ => do
   let matcherApp ← mkConstWithLevelParams matcherConst.name
   let matcherApp := mkAppN matcherApp xs
   let some matcherApp ← matchMatcherApp? matcherApp | throwError "not a matcher app: {matcherApp}"
@@ -931,10 +931,10 @@ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts
     let numParams := altNumParams[i]
     let typeNew ← whnfD typeNew
     match typeNew with
-    | Expr.forallE n d b _ =>
+    | Expr.forallE _ d b _ =>
       let alt ← forallBoundedTelescope d (some numParams) fun xs d => do
         let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
-        forallBoundedTelescope d (some 1) fun x d => do
+        forallBoundedTelescope d (some 1) fun x _ => do
           let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
           mkLambdaFVars xs alt
       updateAlts (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) (i+1)
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index cadf2fd5e2..a1aa8c2513 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -84,7 +84,7 @@ private def getOffset (e : Expr) : OptionT MetaM (Expr × Nat) :=
   getOffsetAux e true
 
 private partial def isOffset : Expr → OptionT MetaM (Expr × Nat)
-  | e@(Expr.app _ a _) =>
+  | e@(Expr.app _ _ _) =>
     let f := e.getAppFn
     match f with
     | Expr.mvar .. => withInstantiatedMVars e isOffset
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 764033638e..fbff429ec8 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -266,7 +266,7 @@ structure SubgoalsResult where
 
 private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr)
     : Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult
-  | args, j, subgoals, instVal, Expr.forallE n d b c => do
+  | args, j, subgoals, instVal, Expr.forallE _ d b c => do
     let d        := d.instantiateRevRange j args.size args
     let mvarType ← mkForallFVars xs d
     let mvar     ← mkFreshExprMVarAt lctx localInsts mvarType
@@ -423,7 +423,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   Remark: This is syntactic check and no reduction is performed.
 -/
 private def hasUnusedArguments : Expr → Bool
-  | Expr.forallE _ d b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
+  | Expr.forallE _ _ b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
   | _ => false
 
 /--
diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index 147b41525a..ab3b1ca54d 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -133,7 +133,7 @@ private def processGenDiseq (mvarId : MVarId) (localDecl : LocalDecl) : MetaM Bo
         if let some (_, lhs, _) ← matchEq? (← inferType arg) then
           unless (← isDefEq arg (← mkEqRefl lhs)) do
             return none
-        if let some (α, lhs, _,  _) ← matchHEq? (← inferType arg) then
+        if let some (_, lhs, _,  _) ← matchHEq? (← inferType arg) then
           unless (← isDefEq arg (← mkHEqRefl lhs)) do
             return none
     let falseProof ← instantiateMVars (mkAppN localDecl.toExpr args)
diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index 757b8bcb27..aea5310ead 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -58,7 +58,7 @@ def apply (s : FVarSubst) (e : Expr) : Expr :=
     | _ => none
 
 def domain (s : FVarSubst) : List FVarId :=
-  s.map.foldl (init := []) fun r k v => k :: r
+  s.map.foldl (init := []) fun r k _ => k :: r
 
 def any (p : FVarId → Expr → Bool) (s : FVarSubst) : Bool :=
   s.map.any p
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index 2d79577080..1fba05f5e7 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -76,7 +76,7 @@ private partial def finalize
         let tag ← getMVarTag mvarId
         if minorIdx ≥ numMinors then throwTacticEx `induction mvarId "ill-formed recursor"
         match recursorType with
-        | Expr.forallE n d b c =>
+        | Expr.forallE n d _ c =>
           let d := d.headBeta
           -- Remark is givenNames is not empty, then user provided explicit alternatives for each minor premise
           if c.binderInfo.isInstImplicit && givenNames.isEmpty then
@@ -181,7 +181,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
         let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type
         majorType.withApp fun majorTypeFn majorTypeArgs => do
           match majorTypeFn with
-          | Expr.const majorTypeFnName majorTypeFnLevels _ => do
+          | Expr.const _               majorTypeFnLevels _ => do
             let majorTypeFnLevels := majorTypeFnLevels.toArray
             let (recursorLevels, foundTargetLevel) ← recursorInfo.univLevelPos.foldlM (init := (#[], false))
                 fun (recursorLevels, foundTargetLevel) (univPos : RecursorUnivLevelPos) => do
diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index cc5c59b806..71649e8bfc 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -32,7 +32,7 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
     let go (type prf : Expr) : MetaM InjectionResultCore := do
       match type.eq? with
       | none           => throwTacticEx `injection mvarId "equality expected"
-      | some (α, a, b) =>
+      | some (_, a, b) =>
         let a ← whnf a
         let b ← whnf b
         let target ← getMVarType mvarId
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 53d4c543a3..2fc749e401 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -202,7 +202,7 @@ inductive SimpLetCase where
   | nondepDepVar -- `let x := v; b` is equivalent to `(fun x => b) v`, but result type depends on `x`
   | nondep -- `let x := v; b` is equivalent to `(fun x => b) v`, and result type does not depend on `x`
 
-def getSimpLetCase (n : Name) (t : Expr) (v : Expr) (b : Expr) : MetaM SimpLetCase := do
+def getSimpLetCase (n : Name) (t : Expr) (_ : Expr) (b : Expr) : MetaM SimpLetCase := do
   withLocalDeclD n t fun x => do
     let bx := b.instantiate1 x
     /- The following step is potentially very expensive when we have many nested let-decls.
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 94ff034156..a2c339b13c 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -86,7 +86,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
      This simple approach was good enough for Mathlib 3 -/
   let mut extraArgs := #[]
   let mut e := e
-  for i in [:numExtraArgs] do
+  for _ in [:numExtraArgs] do
     extraArgs := extraArgs.push e.appArg!
     e := e.appFn!
   extraArgs := extraArgs.reverse
@@ -148,7 +148,7 @@ where
 
 @[inline] def andThen (s : Step) (f? : Expr → SimpM (Option Step)) : SimpM Step := do
   match s with
-  | Step.done r  => return s
+  | Step.done _  => return s
   | Step.visit r =>
     if let some s' ← f? r.expr then
       return s'.updateResult (← mkEqTrans r s'.result)
@@ -186,7 +186,7 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
       if r.isConstOf ``true then
         return some { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
       else if r.isConstOf ``false then
-        let h ← mkEqRefl d
+        let _ ← mkEqRefl d
         return some { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
       else
         return none
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 631e1d1ac6..972ad1fc55 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -147,7 +147,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | 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.letE n₁ t₁ v₁ b₁ _, Expr.letE n₂ t₂ v₂ b₂ _ =>
+  | 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₂
   | s, t => return s == t
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 045fc3cb5e..92871a3788 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -61,7 +61,7 @@ def Step.updateResult : Step → Result → Step
 structure Methods where
   pre        : Expr → SimpM Step          := fun e => return Step.visit { expr := e }
   post       : Expr → SimpM Step          := fun e => return Step.done { expr := e }
-  discharge? : Expr → SimpM (Option Expr) := fun e => return none
+  discharge? : Expr → SimpM (Option Expr) := fun _ => return none
   deriving Inhabited
 
 /- Internal monad -/
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index a14b022d6e..521e62143c 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -62,7 +62,7 @@ private partial def withEqs (lhs rhs : Array Expr) (k : Array Expr → Array Exp
   go 0 #[] #[]
 where
   go (i : Nat) (hs : Array Expr) (rfls : Array Expr) : MetaM α := do
-    if h : i < lhs.size then
+    if _ : i < lhs.size then
       withLocalDeclD (← mkFreshUserName `heq) (← mkEqHEq lhs[i] rhs[i]) fun h => do
         let rfl ← if (← inferType h).isEq then mkEqRefl lhs[i] else mkHEqRefl lhs[i]
         go (i+1) (hs.push h) (rfls.push rfl)
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index df9d46dfaf..bacf343a41 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -22,7 +22,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
     let hLocalDecl ← getLocalDecl hFVarId
     match (← matchEq? hLocalDecl.type) with
     | none => throwTacticEx `subst mvarId "argument must be an equality proof"
-    | some (α, lhs, rhs) => do
+    | some (_, lhs, rhs) => do
       let a ← instantiateMVars <| if symm then rhs else lhs
       let b ← instantiateMVars <| if symm then lhs else rhs
       match a with
@@ -64,7 +64,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
             let hLocalDecl ← getLocalDecl hFVarId
             match (← matchEq? hLocalDecl.type) with
             | none => unreachable!
-            | some (α, lhs, rhs) => do
+            | some (_, lhs, rhs) => do
               let b        ← instantiateMVars <| if symm then lhs else rhs
               let mctx     ← getMCtx
               let depElim := mctx.exprDependsOn mvarDecl.type hFVarId
@@ -145,7 +145,7 @@ 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 (_, lhs, rhs) => substEq mvarId h
     | none => match (← matchHEq? localDecl.type) with
       | some (_, lhs, _, rhs) =>
         let (h', mvarId') ← heqToEq mvarId h
@@ -192,7 +192,7 @@ where
          return none
        else
          match (← matchEq? localDecl.type) with
-         | some (α, lhs, rhs) =>
+         | some (_, lhs, rhs) =>
            let lhs ← instantiateMVars lhs
            let rhs ← instantiateMVars rhs
            if rhs.isFVar && rhs.fvarId! == h && !mctx.exprDependsOn lhs h then
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 4ba8fc6d92..7cb628afae 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -681,7 +681,7 @@ private def shouldVisit (e : Expr) : M Bool := do
             let lctx := (mctx.getDecl mvarId).lctx
             return lctx.any fun decl => pf decl.fvarId
       | Expr.fvar fvarId _   => return pf fvarId
-      | e                    => pure false
+      | _                    => pure false
   visit e
 
 @[inline] partial def main (mctx : MetavarContext) (pf : FVarId → Bool) (pm : MVarId → Bool) (e : Expr) : M Bool :=
@@ -898,7 +898,7 @@ mutual
     | Expr.letE _ t v b _  => return e.updateLet! (← visit xs t) (← visit xs v) (← visit xs b)
     | Expr.mdata _ b _     => return e.updateMData! (← visit xs b)
     | Expr.app ..          => e.withApp fun f args => elimApp xs f args
-    | Expr.mvar mvarId _   => elimApp xs e #[]
+    | Expr.mvar _      _   => elimApp xs e #[]
     | e                    => return e
 
   private partial def mkAuxMVarType (lctx : LocalContext)  (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do
diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index 12bc9115ab..68f87d6d57 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -108,9 +108,9 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.sepBy1 p sep psep trail             => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
   | ParserDescr.trailingNode k prec lhsPrec d       => return trailingNode.formatter k prec lhsPrec (← interpretParserDescr d)
   | ParserDescr.symbol tk                           => return symbol.formatter tk
-  | ParserDescr.nonReservedSymbol tk includeIdent   => return nonReservedSymbol.formatter tk
+  | ParserDescr.nonReservedSymbol tk _              => return nonReservedSymbol.formatter tk
   | ParserDescr.parser constName                    => combinatorFormatterAttribute.runDeclFor constName
-  | ParserDescr.cat catName prec                    => return categoryParser.formatter catName
+  | ParserDescr.cat catName _                       => return categoryParser.formatter catName
 
 end Formatter
 end PrettyPrinter
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index b3685f60c0..adfef67178 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -345,7 +345,7 @@ def dbgTraceState (label : String) (p : Parser) : Parser where
 @[noinline] def epsilonInfo : ParserInfo :=
   { firstTokens := FirstTokens.epsilon }
 
-@[inline] def checkStackTopFn (p : Syntax → Bool) (msg : String) : ParserFn := fun c s =>
+@[inline] def checkStackTopFn (p : Syntax → Bool) (msg : String) : ParserFn := fun _ s =>
   if p s.stxStack.back then s
   else s.mkUnexpectedError msg
 
@@ -427,7 +427,7 @@ def checkPrecFn (prec : Nat) : ParserFn := fun c s =>
 }
 
 /- Succeeds if `c.lhsPrec >= prec` -/
-def checkLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
+def checkLhsPrecFn (prec : Nat) : ParserFn := fun _ s =>
   if s.lhsPrec >= prec then s
   else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term"
 
@@ -436,7 +436,7 @@ def checkLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
   fn   := checkLhsPrecFn prec
 }
 
-def setLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
+def setLhsPrecFn (prec : Nat) : ParserFn := fun _ s =>
   if s.hasError then s
   else { s with lhsPrec := prec }
 
@@ -1059,7 +1059,7 @@ private def tokenFnAux : ParserFn := fun c s =>
 private def updateCache (startPos : String.Pos) (s : ParserState) : ParserState :=
   -- do not cache token parsing errors, which are rare and usually fatal and thus not worth an extra field in `TokenCache`
   match s with
-  | ⟨stack, lhsPrec, pos, cache, none⟩ =>
+  | ⟨stack, lhsPrec, pos, _,     none⟩ =>
     if stack.size == 0 then s
     else
       let tk := stack.back
@@ -1083,7 +1083,7 @@ def peekTokenAux (c : ParserContext) (s : ParserState) : ParserState × Except P
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let s      := tokenFn [] c s
-  if let some e := s.errorMsg then (s.restore iniSz iniPos, Except.error s)
+  if let some _ := s.errorMsg then (s.restore iniSz iniPos, Except.error s)
   else
     let stx := s.stxStack.back
     (s.restore iniSz iniPos, Except.ok stx)
@@ -1189,7 +1189,7 @@ def checkTailWs (prev : Syntax) : Bool :=
   | SourceInfo.original _ _ trailing _ => trailing.stopPos > trailing.startPos
   | _                                  => false
 
-def checkWsBeforeFn (errorMsg : String) : ParserFn := fun c s =>
+def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := s.stxStack.back
   if checkTailWs prev then s else s.mkError errorMsg
 
@@ -1203,7 +1203,7 @@ def checkTailLinebreak (prev : Syntax) : Bool :=
   | SourceInfo.original _ _ trailing _ => trailing.contains '\n'
   | _ => false
 
-def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun c s =>
+def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := s.stxStack.back
   if checkTailLinebreak prev then s else s.mkError errorMsg
 
@@ -1217,7 +1217,7 @@ private def pickNonNone (stack : Array Syntax) : Syntax :=
   | none => Syntax.missing
   | some stx => stx
 
-def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun c s =>
+def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := pickNonNone s.stxStack
   if checkTailNoWs prev then s else s.mkError errorMsg
 
@@ -1668,7 +1668,7 @@ def setExpected (expected : List String) (p : Parser) : Parser :=
   { fn := setExpectedFn expected p.fn, info := p.info }
 
 def pushNone : Parser :=
-  { fn := fun c s => s.pushSyntax mkNullNode }
+  { fn := fun _ s => s.pushSyntax mkNullNode }
 
 -- We support three kinds of antiquotations: `$id`, `$_`, and `$(t)`, where `id` is a term identifier and `t` is a term.
 def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
@@ -1888,7 +1888,7 @@ def fieldIdxFn : ParserFn := fun c s =>
   }
 
 @[inline] def skip : Parser := {
-  fn   := fun c s => s,
+  fn   := fun _ s => s,
   info := epsilonInfo
 }
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 03b23cfb9d..d99075acf4 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -505,7 +505,7 @@ private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : N
     try
       addToken token attrKind
     catch
-      | Exception.error ref msg => throwError "invalid parser '{declName}', {msg}"
+      | Exception.error _   msg => throwError "invalid parser '{declName}', {msg}"
       | ex => throw ex
   let kinds := parser.info.collectKinds {}
   kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 24ba585b41..77bb2eade3 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -57,7 +57,7 @@ def ppModule (stx : Syntax) : CoreM Format := do
   parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
 
 private partial def noContext : MessageData → MessageData
-  | MessageData.withContext ctx msg => noContext msg
+  | MessageData.withContext _   msg => noContext msg
   | MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
   | MessageData.nest n msg => MessageData.nest n (noContext msg)
   | MessageData.group msg  => MessageData.group (noContext msg)
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 1f3d0c8dfb..2d6254cb07 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -75,7 +75,7 @@ where
   unresolveNameCore (n : Name) : DelabM (Option Name) := do
     let mut revComponents := n.components'
     let mut candidate := Name.anonymous
-    for i in [:revComponents.length] do
+    for _ in [:revComponents.length] do
       match revComponents with
       | [] => return none
       | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest
@@ -211,7 +211,7 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
 -- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
   if not (isCoe (← getExpr)) then failure
-  let e ← getExpr
+  let _ ← getExpr
   match stx with
   | `($fn $arg)   => return arg
   | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
@@ -442,7 +442,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
 def delabLetFun : Delab := do
   let stxV ← withAppArg delab
   withAppFn do
-    let Expr.lam n t b _ ← getExpr | unreachable!
+    let Expr.lam n _ b _ ← getExpr | unreachable!
     let n ← getUnusedName n b
     let stxB ← withBindingBody n delab
     if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 0f320cb098..43bf1ebdd3 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -139,7 +139,7 @@ def returnsPi (motive : Expr) : MetaM Bool := do
 
 def isNonConstFun (motive : Expr) : MetaM Bool := do
   match motive with
-  | Expr.lam name d b _ => isNonConstFun b
+  | Expr.lam _    _ b _ => isNonConstFun b
   | _ => return motive.hasLooseBVars
 
 def isSimpleHOFun (motive : Expr) : MetaM Bool :=
@@ -229,7 +229,7 @@ def isHigherOrder (type : Expr) : MetaM Bool := do
   forallTelescopeReducing type fun xs b => return xs.size > 0 && b.isSort
 
 def isFunLike (e : Expr) : MetaM Bool := do
-  forallTelescopeReducing (← inferType e) fun xs b => return xs.size > 0
+  forallTelescopeReducing (← inferType e) fun xs _ => return xs.size > 0
 
 def isSubstLike (e : Expr) : Bool :=
   e.isAppOfArity ``Eq.ndrec 6 || e.isAppOfArity ``Eq.rec 6
@@ -293,7 +293,7 @@ where
     let mType ← whnf mType
     if not (i < args.size) then return ()
     match fType, mType with
-    | Expr.forallE _ fd fb _, Expr.forallE _ md mb _ => do
+    | Expr.forallE _ fd fb _, Expr.forallE _ _  mb _ => do
       -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here?
       -- if so, I'll need to take a callback
       if fd.isOutParam then
@@ -441,7 +441,7 @@ mutual
           annotateBool `pp.analysis.blockImplicit
 
     analyzeConst : AnalyzeM Unit := do
-      let Expr.const n ls .. ← getExpr | unreachable!
+      let Expr.const _ ls .. ← getExpr | unreachable!
       if !(← read).knowsLevel && !ls.isEmpty then
         -- TODO: this is a very crude heuristic, motivated by https://github.com/leanprover/lean4/issues/590
         unless getPPAnalyzeOmitMax (← getOptions) && ls.any containsBadMax do
@@ -458,7 +458,7 @@ mutual
       withBindingBody Name.anonymous analyze
 
     analyzeLet : AnalyzeM Unit := do
-      let Expr.letE n t v body .. ← getExpr | unreachable!
+      let Expr.letE _ _ v _    .. ← getExpr | unreachable!
       if !(← canBottomUp v) then
         annotateBool `pp.analysis.letVarType
         withLetVarType $ withKnowing true false analyze
@@ -530,11 +530,11 @@ mutual
             modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 
     applyFunBinderHeuristic := do
-      let { f, args, mvars, bInfos, .. } ← read
+      let { _, args, mvars, bInfos, .. } ← read
 
       let rec core (argIdx : Nat) (mvarType : Expr) : AnalyzeAppM Bool := do
         match ← getExpr, mvarType with
-        | Expr.lam .., Expr.forallE n t b .. =>
+        | Expr.lam .., Expr.forallE _ t b .. =>
           let mut annotated := false
           for i in [:argIdx] do
             if ← pure (bInfos[i] == BinderInfo.implicit) <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 216ded06ab..039ba14a5d 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -212,7 +212,7 @@ def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
   orelse.formatter antiP p
 
 @[combinatorFormatter Lean.Parser.withAntiquotSuffixSplice]
-def withAntiquotSuffixSplice.formatter (k : SyntaxNodeKind) (p suffix : Formatter) : Formatter := do
+def withAntiquotSuffixSplice.formatter (_ : SyntaxNodeKind) (p suffix : Formatter) : Formatter := do
   if (← getCur).isAntiquotSuffixSplice then
     visitArgs <| suffix *> p
   else
@@ -272,10 +272,10 @@ def errorAtSavedPos.formatter (msg : String) (delta : Bool) : Formatter := pure
 @[combinatorFormatter Lean.Parser.atomic]
 def atomic.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.lookahead]
-def lookahead.formatter (p : Formatter) : Formatter := pure ()
+def lookahead.formatter (_ : Formatter) : Formatter := pure ()
 
 @[combinatorFormatter Lean.Parser.notFollowedBy]
-def notFollowedBy.formatter (p : Formatter) : Formatter := pure ()
+def notFollowedBy.formatter (_ : Formatter) : Formatter := pure ()
 
 @[combinatorFormatter Lean.Parser.andthen]
 def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1
@@ -497,7 +497,7 @@ def interpolatedStr.formatter (p : Formatter) : Formatter := do
 
 @[combinatorFormatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (label : String) (p : Formatter) : Formatter := p
 
-@[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
+@[combinatorFormatter ite, macroInline] def ite {_ : Type} (c : Prop) [_ : Decidable c] (t e : Formatter) : Formatter :=
   if c then t else e
 
 abbrev FormatterAliasValue := AliasValue Formatter
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 3415c37dae..8302fc5fbc 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -288,7 +288,7 @@ def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do
     p
 
 @[combinatorParenthesizer Lean.Parser.withAntiquotSuffixSplice]
-def withAntiquotSuffixSplice.parenthesizer (k : SyntaxNodeKind) (p suffix : Parenthesizer) : Parenthesizer := do
+def withAntiquotSuffixSplice.parenthesizer (_ : SyntaxNodeKind) (p suffix : Parenthesizer) : Parenthesizer := do
   if (← getCur).isAntiquotSuffixSplice then
     visitArgs <| suffix *> p
   else
@@ -366,11 +366,11 @@ def atomic.parenthesizer (p : Parenthesizer) : Parenthesizer :=
   p
 
 @[combinatorParenthesizer Lean.Parser.lookahead]
-def lookahead.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+def lookahead.parenthesizer (_ : Parenthesizer) : Parenthesizer :=
   pure ()
 
 @[combinatorParenthesizer Lean.Parser.notFollowedBy]
-def notFollowedBy.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+def notFollowedBy.parenthesizer (_ : Parenthesizer) : Parenthesizer :=
   pure ()
 
 @[combinatorParenthesizer Lean.Parser.andthen]
@@ -505,7 +505,7 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
 
 @[combinatorParenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (label : String) (p : Parenthesizer) : Parenthesizer := p
 
-@[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
+@[combinatorParenthesizer ite, macroInline] def ite {_ : Type} (c : Prop) [_ : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
   if c then t else e
 
 open Parser
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index 6dbc37a5b6..3a9d33a7d1 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -128,7 +128,7 @@ def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Envi
 def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
   let s := ext.ext.getState env
   match s.stateStack with
-  | state₁ :: state₂ :: stack => ext.ext.setState env { s with stateStack := state₂ :: stack }
+  | _      :: state₂ :: stack => ext.ext.setState env { s with stateStack := state₂ :: stack }
   | _ => env
 
 def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
@@ -208,7 +208,7 @@ def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α
     mkInitial      := return descr.initial
     addEntry       := descr.addEntry
     toOLeanEntry   := id
-    ofOLeanEntry   := fun s a => return a
+    ofOLeanEntry   := fun _ a => return a
     finalizeImport := descr.finalizeImport
   }
 
diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index ced5406875..5c0bb67b67 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -109,7 +109,7 @@ partial def updateFinishedPrefix : AsyncList ε α → BaseIO (AsyncList ε α 
 private partial def finishedPrefixAux : List α → AsyncList ε α → List α
   | acc, cons hd tl   => finishedPrefixAux (hd :: acc) tl
   | acc, nil          => acc
-  | acc, asyncTail tl => acc
+  | acc, asyncTail _  => acc
 
 /-- The longest already-computed prefix of the list. -/
 def finishedPrefix : AsyncList ε α → List α :=
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index d61b1ad425..09da7a3509 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -215,7 +215,7 @@ def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M
     unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names
       for openDecl in ctx.openDecls do
         match openDecl with
-        | OpenDecl.simple ns' except =>
+        | OpenDecl.simple ns' _      =>
           if let some score := matchNamespace ns (ns' ++ id) danglingDot then
             add ns ns' score
             return ()
@@ -288,7 +288,7 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI
       unless (← isBlackListed resolvedId) do
         if let some score := matchAtomic id openedId then
           addCompletionItemForDecl openedId resolvedId expectedType? score
-    | OpenDecl.simple ns except =>
+    | OpenDecl.simple ns _      =>
       getAliasState env |>.forM fun alias declNames => do
         if let some score := matchAlias ns alias then
           addAlias alias declNames score
@@ -417,7 +417,7 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
     match info with
     | CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
-    | CompletionInfo.id stx id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
+    | CompletionInfo.id _   id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
     | CompletionInfo.option stx => optionCompletion ctx stx caps
     | CompletionInfo.tactic .. => tacticCompletion ctx
     | _ => return none
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 2b261eb2f7..972920c3b0 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -360,7 +360,7 @@ end NotificationHandling
 /-! Requests here are handled synchronously rather than in the asynchronous `RequestM`. -/
 section RequestHandling
 
-def handleRpcConnect (p : RpcConnectParams) : WorkerM RpcConnected := do
+def handleRpcConnect (_ : RpcConnectParams) : WorkerM RpcConnected := do
   let (newId, newSesh) ← RpcSession.new
   let newSeshRef ← IO.mkRef newSesh
   modify fun st => { st with rpcSessions := st.rpcSessions.insert newId newSeshRef }
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index bebf2801be..092c259914 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -235,7 +235,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
       return #[]
 
 open Parser.Command in
-partial def handleDocumentSymbol (p : DocumentSymbolParams)
+partial def handleDocumentSymbol (_ : DocumentSymbolParams)
     : RequestM (RequestTask DocumentSymbolResult) := do
   let doc ← readDoc
   asTask do
@@ -388,7 +388,7 @@ where
           lastLspPos := lspPos'
         }
 
-def handleSemanticTokensFull (p : SemanticTokensParams)
+def handleSemanticTokensFull (_ : SemanticTokensParams)
     : RequestM (RequestTask SemanticTokens) := do
   handleSemanticTokens 0 ⟨1 <<< 16⟩
 
@@ -400,7 +400,7 @@ def handleSemanticTokensRange (p : SemanticTokensRangeParams)
   let endPos := text.lspPosToUtf8Pos p.range.end
   handleSemanticTokens beginPos endPos
 
-partial def handleFoldingRange (p : FoldingRangeParams)
+partial def handleFoldingRange (_ : FoldingRangeParams)
   : RequestM (RequestTask (Array FoldingRange)) := do
   let doc ← readDoc
   let t ← doc.allSnaps.waitAll
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 1651d9f663..fde3ed0818 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -32,7 +32,7 @@ partial def InfoTree.visitM [Monad m] [Inhabited α]
   go none
 where go
   | _, context ctx t => go ctx t
-  | some ctx, n@(node i cs) => do
+  | some ctx, _@(node i cs) => do
     preNode ctx i cs
     let as ← cs.toList.mapM (go <| i.updateContext? ctx)
     postNode ctx i cs as
@@ -287,7 +287,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
     | InfoTree.node i@(Info.ofTacticInfo _) cs => Id.run do
-      if let `(by $t) := i.stx then
+      if let `(by $_) := i.stx then
         return false  -- ignore term-nested proofs such as in `simp [show p by ...]`
       if let (some pos', some tailPos') := (i.pos?, i.tailPos?) then
         -- ignore preceding nested infos
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 060de9ab87..c46d06fa98 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -639,7 +639,7 @@ section MainLoop
       | Message.notification method (some params) =>
         handleNotification method (toJson params)
         mainLoop (←runClientTask)
-      | Message.response "register_ilean_watcher" result =>
+      | Message.response "register_ilean_watcher" _      =>
         mainLoop (←runClientTask)
       | _ => throwServerError "Got invalid JSON-RPC message"
     | ServerEvent.clientError e => throw e
@@ -650,7 +650,7 @@ section MainLoop
         mainLoop clientTask
       | WorkerEvent.ioError e =>
         throwServerError s!"IO error while processing events for {fw.doc.meta.uri}: {e}"
-      | WorkerEvent.crashed e =>
+      | WorkerEvent.crashed _ =>
         handleCrash fw.doc.meta.uri #[]
         mainLoop clientTask
       | WorkerEvent.terminated =>
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index f09fbdec2a..158713d370 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -236,7 +236,7 @@ partial instance : ForIn m TopDown Syntax where
       match (← f stx b) with
       | ForInStep.yield b' =>
         let mut b := b'
-        if let Syntax.node i k args := stx then
+        if let Syntax.node _ k args := stx then
           if firstChoiceOnly && k == choiceKind then
             return ← loop args[0] b
           else
@@ -256,7 +256,7 @@ partial def reprint (stx : Syntax) : Option String := do
     match stx with
     | atom info val           => s := s ++ reprintLeaf info val
     | ident info rawVal _ _   => s := s ++ reprintLeaf info rawVal.toString
-    | node info kind args     =>
+    | node _    kind args     =>
       if kind == choiceKind then
         -- this visit the first arg twice, but that should hardly be a problem
         -- given that choice nodes are quite rare and small
diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean
index 223a8dfd36..5044cca631 100644
--- a/src/Lean/Util/FindExpr.lean
+++ b/src/Lean/Util/FindExpr.lean
@@ -41,7 +41,7 @@ unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM
       | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
       | Expr.app f a _         => visit f <|> visit a
       | Expr.proj _ _ b _      => visit b
-      | e                      => failure
+      | _                      => failure
   visit e
 
 
@@ -65,7 +65,7 @@ def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
     | Expr.letE _ t v b _    => find? p t <|> find? p v <|> find? p b
     | Expr.app f a _         => find? p f <|> find? p a
     | Expr.proj _ _ b _      => find? p b
-    | e                      => none
+    | _                      => none
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
@@ -103,7 +103,7 @@ where
         | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
         | Expr.app ..            => visitApp e
         | Expr.proj _ _ b _      => visit b
-        | e                      => failure
+        | _                      => failure
 
 unsafe def findUnsafe? (p : Expr → FindStep) (e : Expr) : Option Expr :=
   Id.run <| findM? p FindImpl.cacheSize e |>.run' FindImpl.initCache
diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean
index 06bc4e7ff9..7d410c9cd1 100644
--- a/src/Lean/Util/FindLevelMVar.lean
+++ b/src/Lean/Util/FindLevelMVar.lean
@@ -34,7 +34,7 @@ mutual
     | Level.succ l _      => visitLevel p l
     | Level.max l₁ l₂ _   => visitLevel p l₁ ∘ visitLevel p l₂
     | Level.imax l₁ l₂ _  => visitLevel p l₁ ∘ visitLevel p l₂
-    | Level.param n _     => id
+    | Level.param _ _     => id
     | Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
 end
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 743bb1f32c..7857bc9300 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -22,8 +22,8 @@ class MonadCache (α β : Type) (m : Type → Type) where
     pure b
 
 instance {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) where
-  findCached? a r := MonadCache.findCached? a
-  cache a b r := MonadCache.cache a b
+  findCached? a _ := MonadCache.findCached? a
+  cache a b _ := MonadCache.cache a b
 
 instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) where
   findCached? a := ExceptT.lift $ MonadCache.findCached? a
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 01b1b5781b..8b19edd1d0 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -22,7 +22,7 @@ where
   go : Name → FilePath
   | Name.str p h _ => go p / h
   | Name.anonymous => base
-  | Name.num p _ _ => panic! "ill-formed import"
+  | Name.num _ _ _ => panic! "ill-formed import"
 
 /-- A `.olean' search path. -/
 abbrev SearchPath := System.SearchPath
@@ -131,7 +131,7 @@ def searchModuleNameOfFileName (fname : FilePath) (rootDirs : SearchPath) : IO (
       return some <| ← moduleNameOfFileName fname <| some rootDir
     catch
       -- Try the next one
-      | e => pure ()
+      | _ => pure ()
   return none
 
 /--
diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean
index 10629e4b45..ca117e5473 100644
--- a/src/Lean/Util/ReplaceLevel.lean
+++ b/src/Lean/Util/ReplaceLevel.lean
@@ -50,7 +50,7 @@ unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr
         | Expr.app f a _         => cache i e <| e.updateApp! (← visit f) (← visit a)
         | Expr.proj _ _ b _      => cache i e <| e.updateProj! (← visit b)
         | Expr.sort u _          => cache i e <| e.updateSort! (u.replace f?)
-        | Expr.const n us _      => cache i e <| e.updateConst! (us.map (Level.replace f?))
+        | Expr.const _ us _      => cache i e <| e.updateConst! (us.map (Level.replace f?))
         | e                      => pure e
   visit e
 
@@ -72,7 +72,7 @@ partial def replaceLevel (f? : Level → Option Level) : Expr → Expr
   | e@(Expr.app f a _)         => let f := replaceLevel f? f; let a := replaceLevel f? a; e.updateApp! f a
   | e@(Expr.proj _ _ b _)      => let b := replaceLevel f? b; e.updateProj! b
   | e@(Expr.sort u _)          => e.updateSort! (u.replace f?)
-  | e@(Expr.const n us _)      => e.updateConst! (us.map (Level.replace f?))
+  | e@(Expr.const _ us _)      => e.updateConst! (us.map (Level.replace f?))
   | e                          => e
 
 end Expr
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 14b89ff72b..4aa74ef82e 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -133,7 +133,7 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
     | EmbedFmt.expr ctx infos =>
       let subTt' := tagExprInfos ctx infos subTt
       return TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
-    | EmbedFmt.goal ctx lctx g =>
+    | EmbedFmt.goal _   _    _ =>
       -- TODO(WN): use InteractiveGoal types here
       unreachable!
     | EmbedFmt.lazyTrace nCtx ctx? cls m =>
diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean
index 6073f8f91d..40ad8880fa 100644
--- a/src/Lean/Widget/TaggedText.lean
+++ b/src/Lean/Widget/TaggedText.lean
@@ -29,7 +29,7 @@ def appendText (s₀ : String) : TaggedText α → TaggedText α
   | text s    => text (s ++ s₀)
   | append as => match as.back with
     | text s => append <| as.set! (as.size - 1) <| text (s ++ s₀)
-    | a      => append <| as.push (text s₀)
+    | _      => append <| as.push (text s₀)
   | a         => append #[a, text s₀]
 
 def appendTag (acc : TaggedText α) (t₀ : α) (a₀ : TaggedText α) : TaggedText α :=
diff --git a/src/Std/Data/AssocList.lean b/src/Std/Data/AssocList.lean
index 7e11eee260..0a829930e2 100644
--- a/src/Std/Data/AssocList.lean
+++ b/src/Std/Data/AssocList.lean
@@ -65,7 +65,7 @@ def find? [BEq α] (a : α) : AssocList α β → Option β
 
 def contains [BEq α] (a : α) : AssocList α β → Bool
   | nil         => false
-  | cons k v es => k == a || contains a es
+  | cons k _ es => k == a || contains a es
 
 def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β
   | nil         => nil
diff --git a/src/Std/Data/DList.lean b/src/Std/Data/DList.lean
index 970f668ab9..5c37e3071b 100644
--- a/src/Std/Data/DList.lean
+++ b/src/Std/Data/DList.lean
@@ -23,17 +23,17 @@ def ofList (l : List α) : DList α :=
   ⟨(l ++ ·), fun t => by simp⟩
 
 def empty : DList α :=
-  ⟨id, fun t => rfl⟩
+  ⟨id, fun _ => rfl⟩
 
 instance : EmptyCollection (DList α) :=
   ⟨DList.empty⟩
 
 def toList : DList α → List α
-  | ⟨f, h⟩ => f []
+  | ⟨f, _⟩ => f []
 
 def singleton (a : α) : DList α := {
   apply     := fun t => a :: t,
-  invariant := fun t => rfl
+  invariant := fun _ => rfl
 }
 
 def cons : α → DList α → DList α
diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean
index a574937250..4d28c21763 100644
--- a/src/Std/Data/PersistentArray.lean
+++ b/src/Std/Data/PersistentArray.lean
@@ -140,7 +140,7 @@ private def emptyArray {α : Type u} : Array (PersistentArrayNode α) :=
   Array.mkEmpty PersistentArray.branching.toNat
 
 partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)
-  | n@(node cs) =>
+  | _@(node cs) =>
     if h : cs.size ≠ 0 then
       let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.pred_lt h⟩
       let last := cs.get idx
@@ -350,7 +350,7 @@ partial def collectStats : PersistentArrayNode α → Stats → Nat → Stats
       { s with
         numNodes := s.numNodes + 1,
         depth    := Nat.max d s.depth }
-  | leaf vs, s, d => { s with numNodes := s.numNodes + 1, depth := Nat.max d s.depth }
+  | leaf _,  s, d => { s with numNodes := s.numNodes + 1, depth := Nat.max d s.depth }
 
 def stats (r : PersistentArray α) : Stats :=
   collectStats r.root { numNodes := 0, depth := 0, tailSize := r.tail.size } 0
@@ -363,7 +363,7 @@ instance : ToString Stats := ⟨Stats.toString⟩
 end PersistentArray
 
 def mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α :=
-  n.fold (init := PersistentArray.empty) fun i p => p.push v
+  n.fold (init := PersistentArray.empty) fun _ p => p.push v
 
 @[inline] def mkPArray {α : Type u} (n : Nat) (v : α) : PArray α :=
   mkPersistentArray n v
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index 7c6f1dacc8..f85caf480c 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/src/Std/Data/PersistentHashMap.lean
@@ -189,7 +189,7 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
     match entries.get! j with
     | Entry.null       => false
     | Entry.ref node   => containsAux node (div2Shift h shift) k
-    | Entry.entry k' v => k == k'
+    | Entry.entry k' _ => k == k'
   | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
 
 def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
@@ -229,7 +229,7 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
     let entry   := entries.get! j
     match entry with
     | Entry.null       => (n, false)
-    | Entry.entry k' v =>
+    | Entry.entry k' _ =>
       if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
     | Entry.ref node   =>
       let entries := entries.set! j Entry.null
diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean
index d3143107e2..de9a80682a 100644
--- a/src/Std/Data/RBMap.lean
+++ b/src/Std/Data/RBMap.lean
@@ -25,12 +25,12 @@ def depth (f : Nat → Nat → Nat) : RBNode α β → Nat
 protected def min : RBNode α β → Option (Sigma (fun k => β k))
   | leaf              => none
   | node _ leaf k v _ => some ⟨k, v⟩
-  | node _ l k v _    => RBNode.min l
+  | node _ l _ _ _    => RBNode.min l
 
 protected def max : RBNode α β → Option (Sigma (fun k => β k))
   | leaf              => none
   | node _ _ k v leaf => some ⟨k, v⟩
-  | node _ _ k v r    => RBNode.max r
+  | node _ _ _ _ r    => RBNode.max r
 
 @[specialize] def fold (f : σ → (k : α) → β k → σ) : (init : σ) → RBNode α β → σ
   | b, leaf           => b
@@ -195,7 +195,7 @@ section Membership
 variable (cmp : α → α → Ordering)
 
 @[specialize] def findCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
-  | leaf,             x => none
+  | leaf,             _ => none
   | node _ a ky vy b, x =>
     match cmp x ky with
     | Ordering.lt => findCore a x
@@ -203,7 +203,7 @@ variable (cmp : α → α → Ordering)
     | Ordering.eq => some ⟨ky, vy⟩
 
 @[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β
-  | leaf,             x => none
+  | leaf,             _ => none
   | node _ a ky vy b, x =>
     match cmp x ky with
     | Ordering.lt => find a x
@@ -211,7 +211,7 @@ variable (cmp : α → α → Ordering)
     | Ordering.eq => some vy
 
 @[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
-  | leaf,             x, lb => lb
+  | leaf,             _, lb => lb
   | node _ a ky vy b, x, lb =>
     match cmp x ky with
     | Ordering.lt => lowerBound a x lb
@@ -299,7 +299,7 @@ instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
   | []        => mkRBMap ..
   | ⟨k,v⟩::xs => (ofList xs).insert k v
 
-@[inline] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
+@[inline] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (_ : α) => β))
   | ⟨t, _⟩, x => t.findCore cmp x
 
 @[inline] def find? : RBMap α β cmp → α → Option β
@@ -310,7 +310,7 @@ instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
 
 /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
     if it exists. -/
-@[inline] def lowerBound : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
+@[inline] def lowerBound : RBMap α β cmp → α → Option (Sigma (fun (_ : α) => β))
   | ⟨t, _⟩, x => t.lowerBound cmp x none
 
 @[inline] def contains (t : RBMap α β cmp) (a : α) : Bool :=