diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index c8fc1f0be9..55ded469fc 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -52,7 +52,7 @@ protected theorem trivial [Applicative m] [LawfulApplicative m] {x : m α} :
 /-- The `SatisfiesM p x` predicate is monotonic in `p`. -/
 theorem imp [Functor m] [LawfulFunctor m] {x : m α}
     (h : SatisfiesM p x) (H : ∀ {a}, p a → q a) : SatisfiesM q x :=
-  let ⟨x, h⟩ := h; ⟨(fun ⟨a, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
+  let ⟨x, h⟩ := h; ⟨(fun ⟨_, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
 
 /-- `SatisfiesM` distributes over `<$>`, general version. -/
 protected theorem map [Functor m] [LawfulFunctor m] {x : m α}
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index c2d76ed0e6..29061c409e 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -758,7 +758,7 @@ where
   | x::xs, n+1, acc => go m xs n (acc.push x)
 
 theorem dropSlice_zero₂ : ∀ n l, @dropSlice α n 0 l = l
-  | 0, [] | 0, _::_ | n+1, [] => rfl
+  | 0, [] | 0, _::_ | _+1, [] => rfl
   | n+1, x::xs => by simp [dropSlice, dropSlice_zero₂]
 
 @[csimp] theorem dropSlice_eq_dropSliceTR : @dropSlice = @dropSliceTR := by
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index ce439cffc5..f03e693d16 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -85,8 +85,8 @@ theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l
 
 theorem eraseIdx_eq_modifyNthTail : ∀ n (l : List α), eraseIdx l n = modifyNthTail tail n l
   | 0, l => by cases l <;> rfl
-  | n+1, [] => rfl
-  | n+1, a :: l => congrArg (cons _) (eraseIdx_eq_modifyNthTail _ _)
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyNthTail _ _)
 
 @[deprecated (since := "2024-05-06")] alias removeNth_eq_nth_tail := eraseIdx_eq_modifyNthTail
 
@@ -171,8 +171,8 @@ theorem modifyNth_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
 
 theorem set_eq_modifyNth (a : α) : ∀ n (l : List α), set l n a = modifyNth (fun _ => a) n l
   | 0, l => by cases l <;> rfl
-  | n+1, [] => rfl
-  | n+1, b :: l => congrArg (cons _) (set_eq_modifyNth _ _ _)
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (cons _) (set_eq_modifyNth _ _ _)
 
 theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
     set l n a = take n l ++ a :: drop (n + 1) l := by
@@ -181,7 +181,7 @@ theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
 theorem modifyNth_eq_set_get? (f : α → α) :
     ∀ n (l : List α), l.modifyNth f n = ((fun a => l.set n (f a)) <$> l.get? n).getD l
   | 0, l => by cases l <;> rfl
-  | n+1, [] => rfl
+  | _+1, [] => rfl
   | n+1, b :: l =>
     (congrArg (cons _) (modifyNth_eq_set_get? ..)).trans <| by cases h : l[n]? <;> simp [h]
 
@@ -293,10 +293,10 @@ theorem replaceF_of_forall_none {l : List α} (h : ∀ a, a ∈ l → p a = none
   | nil => rfl
   | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]
 
-theorem exists_of_replaceF : ∀ {l : List α} {a a'} (al : a ∈ l) (pa : p a = some a'),
+theorem exists_of_replaceF : ∀ {l : List α} {a a'} (_ : a ∈ l) (_ : p a = some a'),
     ∃ a a' l₁ l₂,
       (∀ b ∈ l₁, p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ l.replaceF p = l₁ ++ a' :: l₂
-  | b :: l, a, a', al, pa =>
+  | b :: l, _, _, al, pa =>
     match pb : p b with
     | some b' => ⟨b, b', [], l, forall_mem_nil _, pb, by simp [pb]⟩
     | none =>
@@ -489,7 +489,7 @@ theorem Sublist.diff_right : ∀ {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l
 
 theorem Sublist.erase_diff_erase_sublist {a : α} :
     ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
-  | [], l₂, _ => erase_sublist _ _
+  | [], _, _ => erase_sublist _ _
   | b :: l₁, l₂, h => by
     if heq : b = a then
       simp [heq]
diff --git a/Batteries/Data/RBMap/Alter.lean b/Batteries/Data/RBMap/Alter.lean
index 1148221081..3f6d25c2b3 100644
--- a/Batteries/Data/RBMap/Alter.lean
+++ b/Batteries/Data/RBMap/Alter.lean
@@ -204,7 +204,7 @@ theorem _root_.Batteries.RBNode.Ordered.zoom {t : RBNode α}
 
 theorem Ordered.ins : ∀ {path : Path α} {t : RBNode α},
     t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.ins t).Ordered cmp
-  | .root, t, ht, _, _ => Ordered.setBlack.2 ht
+  | .root, _, ht, _, _ => Ordered.setBlack.2 ht
   | .left red parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
     unfold ins; have ⟨ax, ap⟩ := All_and.1 H; exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .right red a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
@@ -222,7 +222,7 @@ theorem Ordered.insertNew {path : Path α} (hp : path.Ordered cmp) (vp : path.Ro
 
 theorem Ordered.del : ∀ {path : Path α} {t : RBNode α} {c},
     t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.del t c).Ordered cmp
-  | .root, t, _, ht, _, _ => Ordered.setBlack.2 ht
+  | .root, _, _, ht, _, _ => Ordered.setBlack.2 ht
   | .left _ parent x b, a, red, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
     unfold del; have ⟨ax, ap⟩ := All_and.1 H; exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .right _ a x parent, b, red, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean
index 9d7d14a70d..f8fe5a6e38 100644
--- a/Batteries/Logic.lean
+++ b/Batteries/Logic.lean
@@ -31,7 +31,7 @@ end Classical
 theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
-    (@Eq.rec α a (fun α _ => β) y a' h) = y := by cases h; rfl
+    (@Eq.rec α a (fun _ _ => β) y a' h) = y := by cases h; rfl
 
 theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
diff --git a/Batteries/WF.lean b/Batteries/WF.lean
index 73428fe3bd..2c36dccebd 100644
--- a/Batteries/WF.lean
+++ b/Batteries/WF.lean
@@ -50,7 +50,7 @@ instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
     {a : α} (t : Acc r a) : motive a t :=
-  intro a (fun x h => t.inv h) (fun y hr => recC intro (t.inv hr))
+  intro a (fun _ h => t.inv h) (fun _ hr => recC intro (t.inv hr))
 termination_by Subtype.mk a t
 
 unseal recC