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/Basic.lean b/src/Init/Control/Basic.lean
index 31b4858e0b..f4630fb3e0 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -208,7 +208,7 @@ instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
   restoreM x := pure x
 
 @[inline]
-def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : Bind n] {α : Type u}
+def controlAt (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   liftWith f >>= restoreM
 
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 55d88ec54f..eddf6c602f 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -27,7 +27,7 @@ end ReaderT
 instance : MonadControl m (ReaderT ρ m) where
   stM      := id
   liftWith f ctx := f fun x => x ctx
-  restoreM x ctx := x
+  restoreM x _ := x
 
 instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
   tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5adaec8196..a9746d0347 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -149,14 +149,17 @@ def Priority.max : Priority := 8
   non-dedicated workers than the number of cores to reduce context switches. -/
 def Priority.dedicated : Priority := 9
 
+set_option linter.unusedVariables.funArgs false in
 @[noinline, extern "lean_task_spawn"]
 protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
   ⟨fn ()⟩
 
+set_option linter.unusedVariables.funArgs false in
 @[noinline, extern "lean_task_map"]
 protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β :=
   ⟨f x.get⟩
 
+set_option linter.unusedVariables.funArgs false in
 @[noinline, extern "lean_task_bind"]
 protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β :=
   ⟨(f x.get).get⟩
@@ -424,7 +427,7 @@ end Decidable
 
 section
 variable {p q : Prop}
-@[inline] def  decidable_of_decidable_of_iff [hp : Decidable p] (h : p ↔ q) : Decidable q :=
+@[inline] def  decidable_of_decidable_of_iff [Decidable p] (h : p ↔ q) : Decidable q :=
   if hp : p then
     isTrue (Iff.mp h hp)
   else
@@ -501,7 +504,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
     (motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
     (inst (f x) (f y))
     (fun h' => False.elim (h' (congrArg f h)))
-    (fun h' => fun x => x)
+    (fun _ => fun x => x)
 
 /- Inhabited -/
 
@@ -554,7 +557,7 @@ structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
   symm  : ∀ {x y}, r x y → r y x
   trans : ∀ {x y z}, r x y → r y z → r x z
 
-def emptyRelation {α : Sort u} (a₁ a₂ : α) : Prop :=
+def emptyRelation {α : Sort u} (_ _ : α) : Prop :=
   False
 
 def Subrelation {α : Sort u} (q r : α → α → Prop) :=
@@ -576,7 +579,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
-  | ⟨_, _ ⟩, ⟨_, _⟩, rfl => rfl
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
@@ -959,7 +962,7 @@ variable   {α : Sort u}
 private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
   Quotient.liftOn₂ q₁ q₂
     (fun a₁ a₂ => a₁ ≈ a₂)
-    (fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ =>
+    (fun _ _ _ _ a₁b₁ a₂b₂ =>
       propext (Iff.intro
         (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
         (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
@@ -1045,7 +1048,7 @@ private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀ (x : α),
 private def extfunApp (f : Quotient <| funSetoid α β) (x : α) : β x :=
   Quot.liftOn f
     (fun (f : ∀ (x : α), β x) => f x)
-    (fun f₁ f₂ h => h x)
+    (fun _ _ h => h x)
 
 theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
   show extfunApp (Quotient.mk' f₁) = extfunApp (Quotient.mk' f₂)
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index fd2ac9cd63..f1b949a9c1 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -200,8 +200,8 @@ 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,   _,   h1, h2 => absurd h1 (Nat.lt_irrefl 0)
-  | _+1, 0,   h1, h2 => absurd h2 (Nat.lt_irrefl 0)
+  | 0,   _,   h1, _  => absurd h1 (Nat.lt_irrefl 0)
+  | _+1, 0,   _, 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
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 177ee28872..780ad4d325 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -111,7 +111,7 @@ 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 _ h₁ =>
       HEq.rec (motive := fun {β} (b : β) (_ : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
-        (fun (h₂ : Eq α α) => rfl)
+        (fun (_ : Eq α α) => rfl)
         h₁
   this α α a a' h rfl
 
@@ -161,6 +161,7 @@ structure Subtype {α : Sort u} (p : α → Prop) where
   val : α
   property : p val
 
+set_option linter.unusedVariables.funArgs false in
 /-- Gadget for optional parameter support. -/
 @[reducible] def optParam (α : Sort u) (default : α) : Sort u := α
 
@@ -385,7 +386,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 -/
@@ -1073,8 +1074,8 @@ instance {α} : Inhabited (List α) where
 
 protected def List.hasDecEq {α: Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
   | nil,       nil       => isTrue rfl
-  | cons _ as, nil       => isFalse (fun h => List.noConfusion h)
-  | nil,       cons _ bs => isFalse (fun h => List.noConfusion h)
+  | cons _ _, nil        => isFalse (fun h => List.noConfusion h)
+  | nil,       cons _ _  => isFalse (fun h => List.noConfusion h)
   | cons a as, cons b bs =>
     match decEq a b with
     | isTrue hab  =>
@@ -2147,7 +2148,7 @@ private def extractImported (scps : List MacroScope) (mainModule : Name) : Name
     match beq str "_@" with
     | true  => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
     | false => extractImported scps mainModule p (List.cons n parts)
-  | n@(Name.num p str _), parts => extractImported scps mainModule p (List.cons n parts)
+  | n@(Name.num p _ _), parts => extractImported scps mainModule p (List.cons n parts)
   | _,                    _     => panic "Error: unreachable @ extractImported"
 
 private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
@@ -2155,7 +2156,7 @@ 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 _ num _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
+  | n@(Name.num _ _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
   | _,                    _   => panic "Error: unreachable @ extractMainModule"
 
 private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 8a1b9f3451..93ac4f80d3 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -30,7 +30,7 @@ variable {α : Sort u} {r : α → α → Prop}
 
 def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
 Acc.recOn (motive := fun (x : α) _ => r y x → Acc r y)
-  h₁ (fun x₁ ac₁ ih h₂ => ac₁ y h₂) h₂
+  h₁ (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
 
@@ -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₁ _   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₁ _   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 _  => exact rfl
+  | intro x r _ => exact rfl
 
 end
 
@@ -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 _  ih =>
+  | intro x _ ih =>
     apply Acc.intro
     intro y h
     exact ih y (h₁ h)
@@ -145,7 +145,7 @@ def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
     intro y rel
     induction rel with
     | base a b rab => exact ih a rab
-    | trans a b c rab rbc ih₁ ih₂ => apply Acc.inv (ih₂ acx ih) rab
+    | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
 
 def wf (h : WellFounded r) : WellFounded (TC r) :=
   ⟨fun a => accessible (apply h a)⟩
@@ -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 _   iha =>
+  | intro xa _ iha =>
     induction (acb b) with
-    | intro xb _   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 _   iha =>
+  | intro xa _ iha =>
     induction (WellFounded.apply (acb xa) b) with
-    | intro xb _   ihb =>
+    | intro xb _ ihb =>
       apply Acc.intro
       intro p lt
       cases lt with
@@ -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 _   ihb =>
+  | intro xb _ ihb =>
     intro a
     induction (aca a) with
-    | intro xa _   iha =>
+    | intro xa _ iha =>
       apply Acc.intro
       intro p lt
       cases lt with