From f70dfcdec4c878c617167f5584c8e23e69298158 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Mon, 30 Sep 2024 00:48:54 +0100
Subject: [PATCH] another batch

---
 Mathlib/Algebra/Module/BigOperators.lean  | 2 +-
 Mathlib/Algebra/Polynomial/Induction.lean | 5 ++---
 Mathlib/Order/Interval/Finset/Basic.lean  | 8 ++++----
 Mathlib/Order/SuccPred/Basic.lean         | 2 +-
 4 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/Module/BigOperators.lean b/Mathlib/Algebra/Module/BigOperators.lean
index 8b68d57357fd4..d15e7274ec57a 100644
--- a/Mathlib/Algebra/Module/BigOperators.lean
+++ b/Mathlib/Algebra/Module/BigOperators.lean
@@ -15,7 +15,7 @@ variable {ι κ α β R M : Type*}
 
 section AddCommMonoid
 
-variable [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x y : M)
+variable [Semiring R] [AddCommMonoid M] [Module R M]
 
 theorem List.sum_smul {l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
   map_list_sum ((smulAddHom R M).flip x) l
diff --git a/Mathlib/Algebra/Polynomial/Induction.lean b/Mathlib/Algebra/Polynomial/Induction.lean
index 4ba0e2bf397db..a4fc244b867ab 100644
--- a/Mathlib/Algebra/Polynomial/Induction.lean
+++ b/Mathlib/Algebra/Polynomial/Induction.lean
@@ -26,12 +26,11 @@ open Polynomial
 
 universe u v w x y z
 
-variable {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z} {a b : R}
-  {m n : ℕ}
+variable {R : Type u}
 
 section Semiring
 
-variable [Semiring R] {p q r : R[X]}
+variable [Semiring R]
 
 @[elab_as_elim]
 protected theorem induction_on {M : R[X] → Prop} (p : R[X]) (h_C : ∀ a, M (C a))
diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean
index 8964e28ae8b2a..53ccb40f79265 100644
--- a/Mathlib/Order/Interval/Finset/Basic.lean
+++ b/Mathlib/Order/Interval/Finset/Basic.lean
@@ -683,7 +683,7 @@ variable [LinearOrder α]
 
 section LocallyFiniteOrder
 
-variable [LocallyFiniteOrder α] {a b : α}
+variable [LocallyFiniteOrder α]
 
 theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
     Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
@@ -790,7 +790,7 @@ end LinearOrder
 
 section Lattice
 
-variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ x : α}
 
 theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding :=
   Icc_toDual _ _
@@ -862,7 +862,7 @@ end Lattice
 
 section DistribLattice
 
-variable [DistribLattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [DistribLattice α] [LocallyFiniteOrder α] {a b c : α}
 
 theorem eq_of_mem_uIcc_of_mem_uIcc : a ∈ [[b, c]] → b ∈ [[a, c]] → a = b := by
   simp_rw [mem_uIcc]
@@ -883,7 +883,7 @@ end DistribLattice
 
 section LinearOrder
 
-variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c : α}
 
 theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
   rfl
diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean
index d8d173cca893a..aef647a6f8d31 100644
--- a/Mathlib/Order/SuccPred/Basic.lean
+++ b/Mathlib/Order/SuccPred/Basic.lean
@@ -927,7 +927,7 @@ lemma gc_pred_succ : GaloisConnection (pred : α → α) succ := fun _ _ ↦ pre
 
 end Preorder
 
-variable [PartialOrder α] [SuccOrder α] [PredOrder α] {a b : α}
+variable [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α}
 
 @[simp]
 theorem succ_pred_of_not_isMin (h : ¬IsMin a) : succ (pred a) = a :=