chore: remove some unused variables (#31017)

Author: Ruben-VandeVelde

Mathlib/Algebra/BigOperators/Group/List/Defs.lean

@@ -13,7 +13,7 @@ which calculate the product and sum of elements of a list
 and `List.alternatingProd`, `List.alternatingSum`, their alternating counterparts.
 -/
 
-variable {ι α β M N P G : Type*}
+variable {ι M N : Type*}
 
 namespace List
 section Defs
@@ -42,14 +42,14 @@ end Defs
 
 section Mul
 
-variable [Mul M] [One M] {l : List M} {a : M}
+variable [Mul M] [One M] {a : M} {l : List M}
 
 @[to_additive existing, simp]
 theorem prod_nil : ([] : List M).prod = 1 :=
   rfl
 
 @[to_additive existing, simp]
-theorem prod_cons {a} {l : List M} : (a :: l).prod = a * l.prod := rfl
+theorem prod_cons : (a :: l).prod = a * l.prod := rfl
 
 @[to_additive]
 lemma prod_induction
@@ -87,7 +87,7 @@ end MulOneClass
 
 section Monoid
 
-variable [Monoid M] [Monoid N] [Monoid P] {l l₁ l₂ : List M} {a : M}
+variable [Monoid M] [Monoid N]
 
 @[to_additive]
 theorem prod_eq_foldr {l : List M} : l.prod = foldr (· * ·) 1 l := rfl