diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean
index 4efe977e0587c..d884a6db4b9f2 100644
--- a/Mathlib/Algebra/Lie/Killing.lean
+++ b/Mathlib/Algebra/Lie/Killing.lean
@@ -38,7 +38,7 @@ This file contains basic definitions and results for such Lie algebras.
 
 -/
 
-variable (R K L M : Type*) [CommRing R] [Field K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L]
+variable (R K L : Type*) [CommRing R] [Field K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L]
 
 namespace LieAlgebra
 
diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
index 42aba8ff24d51..d0a29face182e 100644
--- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
+++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
@@ -171,7 +171,7 @@ open Asymptotics
 
 section NormedField
 
-variable {α β : Type*} [NormedField β] {t u v w : α → β} {l : Filter α}
+variable {α β : Type*} [NormedField β] {u v : α → β} {l : Filter α}
 
 theorem isEquivalent_iff_exists_eq_mul :
     u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v := by
diff --git a/Mathlib/Analysis/Complex/Conformal.lean b/Mathlib/Analysis/Complex/Conformal.lean
index 9c3c4ee064bd1..2163c30f6ec46 100644
--- a/Mathlib/Analysis/Complex/Conformal.lean
+++ b/Mathlib/Analysis/Complex/Conformal.lean
@@ -41,8 +41,7 @@ theorem isConformalMap_conj : IsConformalMap (conjLIE : ℂ →L[ℝ] ℂ) :=
 
 section ConformalIntoComplexNormed
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] {z : ℂ}
-  {g : ℂ →L[ℝ] E} {f : ℂ → E}
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E]
 
 theorem isConformalMap_complex_linear {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
     IsConformalMap (map.restrictScalars ℝ) := by
@@ -70,7 +69,7 @@ section ConformalIntoComplexPlane
 
 open ContinuousLinearMap
 
-variable {f : ℂ → ℂ} {z : ℂ} {g : ℂ →L[ℝ] ℂ}
+variable {g : ℂ →L[ℝ] ℂ}
 
 theorem IsConformalMap.is_complex_or_conj_linear (h : IsConformalMap g) :
     (∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
index 256120e306349..f5899e0495eca 100644
--- a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
+++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
@@ -29,7 +29,7 @@ open scoped UpperHalfPlane ComplexConjugate NNReal Topology MatrixGroups
 
 open Set Metric Filter Real
 
-variable {z w : ℍ} {r R : ℝ}
+variable {z w : ℍ} {r : ℝ}
 
 namespace UpperHalfPlane
 
diff --git a/Mathlib/Analysis/Convex/Integral.lean b/Mathlib/Analysis/Convex/Integral.lean
index dd75c412a4ffc..7d933906dae1b 100644
--- a/Mathlib/Analysis/Convex/Integral.lean
+++ b/Mathlib/Analysis/Convex/Integral.lean
@@ -39,9 +39,8 @@ open MeasureTheory MeasureTheory.Measure Metric Set Filter TopologicalSpace Func
 
 open scoped Topology ENNReal Convex
 
-variable {α E F : Type*} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : Measure α}
-  {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} {C : ℝ}
+variable {α E : Type*} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [CompleteSpace E] {μ : Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} {C : ℝ}
 
 /-!
 ### Non-strict Jensen's inequality
diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean
index 45bc7d0036eb8..9504c21166ab9 100644
--- a/Mathlib/Analysis/Convex/Side.lean
+++ b/Mathlib/Analysis/Convex/Side.lean
@@ -345,7 +345,6 @@ end StrictOrderedCommRing
 section LinearOrderedField
 
 variable [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P]
-variable [AddCommGroup V'] [Module R V'] [AddTorsor V' P']
 
 @[simp]
 theorem wOppSide_self_iff {s : AffineSubspace R P} {x : P} : s.WOppSide x x ↔ x ∈ s := by
diff --git a/Mathlib/Analysis/Convex/Strong.lean b/Mathlib/Analysis/Convex/Strong.lean
index f0301456bebd8..64d17ed42cec3 100644
--- a/Mathlib/Analysis/Convex/Strong.lean
+++ b/Mathlib/Analysis/Convex/Strong.lean
@@ -27,7 +27,7 @@ open Real
 variable {E : Type*} [NormedAddCommGroup E]
 
 section NormedSpace
-variable [NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {a b m : ℝ} {x y : E} {f g : E → ℝ}
+variable [NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {m : ℝ} {f g : E → ℝ}
 
 /-- A function `f` from a real normed space is uniformly convex with modulus `φ` if
 `f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖` for all `t ∈ [0, 1]`.
@@ -145,7 +145,7 @@ nonrec lemma StrongConcaveOn.strictConcaveOn (hf : StrongConcaveOn s m f) (hm :
 end NormedSpace
 
 section InnerProductSpace
-variable [InnerProductSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {a b m : ℝ} {x y : E} {f : E → ℝ}
+variable [InnerProductSpace ℝ E] {s : Set E} {a b m : ℝ} {x y : E} {f : E → ℝ}
 
 private lemma aux_sub (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
     a * (f x - m / (2 : ℝ) * ‖x‖ ^ 2) + b * (f y - m / (2 : ℝ) * ‖y‖ ^ 2) +
diff --git a/Mathlib/Analysis/LocallyConvex/AbsConvex.lean b/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
index c13ab3c9c7b85..f7f1bf219971d 100644
--- a/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
+++ b/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
@@ -49,7 +49,7 @@ open NormedField Set
 
 open NNReal Pointwise Topology
 
-variable {𝕜 E F G ι : Type*}
+variable {𝕜 E : Type*}
 
 section AbsolutelyConvex
 
@@ -103,7 +103,7 @@ theorem absConvexHull_eq_iInter :
     absConvexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : AbsConvex 𝕜 t), t := by
   simp [absConvexHull, iInter_subtype, iInter_and]
 
-variable {t : Set E} {x y : E}
+variable {t : Set E} {x : E}
 
 theorem mem_absConvexHull_iff : x ∈ absConvexHull 𝕜 s ↔ ∀ t, s ⊆ t → AbsConvex 𝕜 t → x ∈ t := by
   simp_rw [absConvexHull_eq_iInter, mem_iInter]
@@ -151,7 +151,7 @@ end AbsolutelyConvex
 
 section NontriviallyNormedField
 
-variable (𝕜 E) {s : Set E}
+variable (𝕜 E)
 variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
 variable [Module ℝ E] [SMulCommClass ℝ 𝕜 E]
 variable [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul 𝕜 E]
diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean
index 8f324581a6270..a3904e3c612c7 100644
--- a/Mathlib/Analysis/LocallyConvex/Bounded.lean
+++ b/Mathlib/Analysis/LocallyConvex/Bounded.lean
@@ -42,7 +42,7 @@ von Neumann-bounded sets.
 -/
 
 
-variable {𝕜 𝕜' E E' F ι : Type*}
+variable {𝕜 𝕜' E F ι : Type*}
 
 open Set Filter Function
 open scoped Topology Pointwise
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
index 13d4746c6c707..879cc599b5765 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
@@ -38,7 +38,7 @@ weak dual, seminorm
 -/
 
 
-variable {𝕜 E F ι : Type*}
+variable {𝕜 E F : Type*}
 
 open Topology
 
@@ -84,8 +84,6 @@ end BilinForm
 section Topology
 
 variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
-variable [Nonempty ι]
-variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}
 
 theorem LinearMap.hasBasis_weakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
     (𝓝 (0 : WeakBilin B)).HasBasis B.toSeminormFamily.basisSets _root_.id := by
@@ -134,7 +132,7 @@ end Topology
 section LocallyConvex
 
 variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
-variable [Nonempty ι] [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
+variable [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
 
 instance WeakBilin.locallyConvexSpace {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} :
     LocallyConvexSpace ℝ (WeakBilin B) :=
diff --git a/Mathlib/Analysis/Normed/Affine/AddTorsor.lean b/Mathlib/Analysis/Normed/Affine/AddTorsor.lean
index 2e2257c96f378..105fcc993b856 100644
--- a/Mathlib/Analysis/Normed/Affine/AddTorsor.lean
+++ b/Mathlib/Analysis/Normed/Affine/AddTorsor.lean
@@ -22,7 +22,7 @@ open NNReal Topology
 
 open Filter
 
-variable {α V P W Q : Type*} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P]
+variable {V P W Q : Type*} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P]
   [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q]
 
 section NormedSpace
diff --git a/Mathlib/Analysis/Normed/Group/Pointwise.lean b/Mathlib/Analysis/Normed/Group/Pointwise.lean
index f06a7d00a7621..8d853167e1370 100644
--- a/Mathlib/Analysis/Normed/Group/Pointwise.lean
+++ b/Mathlib/Analysis/Normed/Group/Pointwise.lean
@@ -22,7 +22,7 @@ variable {E : Type*}
 
 section SeminormedGroup
 
-variable [SeminormedGroup E] {ε δ : ℝ} {s t : Set E} {x y : E}
+variable [SeminormedGroup E] {s t : Set E}
 
 -- note: we can't use `LipschitzOnWith.isBounded_image2` here without adding `[IsometricSMul E E]`
 @[to_additive]
@@ -50,7 +50,7 @@ end SeminormedGroup
 
 section SeminormedCommGroup
 
-variable [SeminormedCommGroup E] {ε δ : ℝ} {s t : Set E} {x y : E}
+variable [SeminormedCommGroup E] {δ : ℝ} {s : Set E} {x y : E}
 
 section EMetric
 
@@ -73,7 +73,7 @@ theorem ediam_mul_le (x y : Set E) : EMetric.diam (x * y) ≤ EMetric.diam x + E
 
 end EMetric
 
-variable (ε δ s t x y)
+variable (δ s x y)
 
 @[to_additive (attr := simp)]
 theorem inv_thickening : (thickening δ s)⁻¹ = thickening δ s⁻¹ := by
@@ -188,7 +188,7 @@ theorem ball_mul : ball x δ * s = x • thickening δ s := by rw [mul_comm, mul
 @[to_additive (attr := simp)]
 theorem ball_div : ball x δ / s = x • thickening δ s⁻¹ := by simp [div_eq_mul_inv]
 
-variable {ε δ s t x y}
+variable {δ s x y}
 
 @[to_additive]
 theorem IsCompact.mul_closedBall_one (hs : IsCompact s) (hδ : 0 ≤ δ) :
diff --git a/Mathlib/Analysis/Normed/Order/UpperLower.lean b/Mathlib/Analysis/Normed/Order/UpperLower.lean
index b30f015561105..8c260c437ed28 100644
--- a/Mathlib/Analysis/Normed/Order/UpperLower.lean
+++ b/Mathlib/Analysis/Normed/Order/UpperLower.lean
@@ -114,7 +114,7 @@ theorem IsLowerSet.mem_interior_of_forall_lt (hs : IsLowerSet s) (hx : x ∈ clo
 end Finite
 
 section Fintype
-variable [Fintype ι] {s t : Set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+variable [Fintype ι] {s : Set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
 
 -- TODO: Generalise those lemmas so that they also apply to `ℝ` and `EuclideanSpace ι ℝ`
 lemma dist_inf_sup_pi (x y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y := by
@@ -184,7 +184,7 @@ theorem IsLowerSet.exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s)
 end Fintype
 
 section Finite
-variable [Finite ι] {s t : Set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+variable [Finite ι] {s : Set (ι → ℝ)}
 
 /-!
 #### Note
diff --git a/Mathlib/Analysis/Normed/Ring/Seminorm.lean b/Mathlib/Analysis/Normed/Ring/Seminorm.lean
index f25dcea804efa..5fdaed6043d37 100644
--- a/Mathlib/Analysis/Normed/Ring/Seminorm.lean
+++ b/Mathlib/Analysis/Normed/Ring/Seminorm.lean
@@ -39,7 +39,7 @@ ring_seminorm, ring_norm
 
 open NNReal
 
-variable {F R S : Type*} (x y : R) (r : ℝ)
+variable {R : Type*}
 
 /-- A seminorm on a ring `R` is a function `f : R → ℝ` that preserves zero, takes nonnegative
   values, is subadditive and submultiplicative and such that `f (-x) = f x` for all `x ∈ R`. -/
diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
index 1c096d7eb792e..d042eab14c553 100644
--- a/Mathlib/Analysis/Seminorm.lean
+++ b/Mathlib/Analysis/Seminorm.lean
@@ -38,7 +38,7 @@ open NormedField Set Filter
 
 open scoped NNReal Pointwise Topology Uniformity
 
-variable {R R' 𝕜 𝕜₂ 𝕜₃ 𝕝 E E₂ E₃ F G ι : Type*}
+variable {R R' 𝕜 𝕜₂ 𝕜₃ 𝕝 E E₂ E₃ F ι : Type*}
 
 /-- A seminorm on a module over a normed ring is a function to the reals that is positive
 semidefinite, positive homogeneous, and subadditive. -/
@@ -138,7 +138,7 @@ theorem zero_apply (x : E) : (0 : Seminorm 𝕜 E) x = 0 :=
 instance : Inhabited (Seminorm 𝕜 E) :=
   ⟨0⟩
 
-variable (p : Seminorm 𝕜 E) (c : 𝕜) (x y : E) (r : ℝ)
+variable (p : Seminorm 𝕜 E) (x : E) (r : ℝ)
 
 /-- Any action on `ℝ` which factors through `ℝ≥0` applies to a seminorm. -/
 instance instSMul [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] : SMul R (Seminorm 𝕜 E) where
@@ -261,8 +261,7 @@ variable {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂]
 variable {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃]
 variable {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₁₃]
 variable [AddCommGroup E] [AddCommGroup E₂] [AddCommGroup E₃]
-variable [AddCommGroup F] [AddCommGroup G]
-variable [Module 𝕜 E] [Module 𝕜₂ E₂] [Module 𝕜₃ E₃] [Module 𝕜 F] [Module 𝕜 G]
+variable [Module 𝕜 E] [Module 𝕜₂ E₂] [Module 𝕜₃ E₃]
 
 -- Porting note: even though this instance is found immediately by typeclass search,
 -- it seems to be needed below!?
@@ -867,8 +866,7 @@ end SeminormedRing
 
 section NormedField
 
-variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {A B : Set E} {a : 𝕜}
-  {r : ℝ} {x : E}
+variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E}
 
 theorem closedBall_iSup {ι : Sort*} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (range p)) (e : E)
     {r : ℝ} (hr : 0 < r) : closedBall (⨆ i, p i) e r = ⋂ i, closedBall (p i) e r := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean
index e11cef64dcdb8..16a6eab99254d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Integrals.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Integrals.lean
@@ -43,7 +43,7 @@ namespace intervalIntegral
 
 open MeasureTheory
 
-variable {f : ℝ → ℝ} {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ] (c d : ℝ)
+variable {f : ℝ → ℝ} {μ : Measure ℝ} [IsLocallyFiniteMeasure μ] (c d : ℝ)
 
 /-! ### Interval integrability -/
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
index c7eaabb0c3580..5aa71529e87e1 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
@@ -25,8 +25,6 @@ noncomputable section
 
 namespace Real
 
-variable {x y : ℝ}
-
 theorem log_mul_self_monotoneOn : MonotoneOn (fun x : ℝ => log x * x) { x | 1 ≤ x } := by
   -- TODO: can be strengthened to exp (-1) ≤ x
   simp only [MonotoneOn, mem_setOf_eq]
diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
index e4f0d3a9330f3..0486eff13103d 100644
--- a/Mathlib/Analysis/SpecificLimits/Normed.lean
+++ b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -27,7 +27,7 @@ noncomputable section
 
 open Set Function Filter Finset Metric Asymptotics Topology Nat NNReal ENNReal
 
-variable {α β ι : Type*}
+variable {α : Type*}
 
 /-! ### Powers -/
 
diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean
index 2408d76270ca3..de7ec32fc5e16 100644
--- a/Mathlib/CategoryTheory/Sites/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Sites/Equivalence.lean
@@ -167,9 +167,6 @@ theorem hasSheafCompose : J.HasSheafCompose F where
       e.functor.op_comp_isSheaf _ _ ⟨_, hP'⟩
     exact (Presheaf.isSheaf_of_iso_iff ((isoWhiskerRight e.op.unitIso.symm (P ⋙ F)))).mp hP'
 
-variable [ConcreteCategory.{w} A]
-variable {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G)
-
 end Equivalence
 
 variable (B : Type u₄) [Category.{v₄} B] (F : A ⥤ B)
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
index e70175d8c7398..131989eef9048 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
@@ -196,8 +196,7 @@ theorem le_bound : l ≤ bound ε l :=
 theorem bound_pos : 0 < bound ε l :=
   (initialBound_pos ε l).trans_le <| initialBound_le_bound ε l
 
-variable {ι 𝕜 : Type*} [LinearOrderedField 𝕜] (r : ι → ι → Prop) [DecidableRel r] {s t : Finset ι}
-  {x : 𝕜}
+variable {ι 𝕜 : Type*} [LinearOrderedField 𝕜] {s t : Finset ι} {x : 𝕜}
 
 theorem mul_sq_le_sum_sq (hst : s ⊆ t) (f : ι → 𝕜) (hs : x ^ 2 ≤ ((∑ i ∈ s, f i) / #s) ^ 2)
     (hs' : (#s : 𝕜) ≠ 0) : (#s : 𝕜) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2 :=
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
index f688f79dda165..d34cb87cc5907 100644
--- a/Mathlib/FieldTheory/Finite/Basic.lean
+++ b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -328,8 +328,6 @@ theorem X_pow_card_pow_sub_X_ne_zero (hn : n ≠ 0) (hp : 1 < p) : (X ^ p ^ n -
 
 end
 
-variable (p : ℕ) [Fact p.Prime] [Algebra (ZMod p) K]
-
 theorem roots_X_pow_card_sub_X : roots (X ^ q - X : K[X]) = Finset.univ.val := by
   classical
     have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
diff --git a/Mathlib/Geometry/Euclidean/Inversion/Basic.lean b/Mathlib/Geometry/Euclidean/Inversion/Basic.lean
index d819c1008538f..f1ccbd341903b 100644
--- a/Mathlib/Geometry/Euclidean/Inversion/Basic.lean
+++ b/Mathlib/Geometry/Euclidean/Inversion/Basic.lean
@@ -32,7 +32,7 @@ variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricS
 
 namespace EuclideanGeometry
 
-variable {a b c d x y z : P} {r R : ℝ}
+variable {c x y : P} {R : ℝ}
 
 /-- Inversion in a sphere in an affine space. This map sends each point `x` to the point `y` such
 that `y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)`, where `c` and `R` are the center and the radius the
diff --git a/Mathlib/LinearAlgebra/Matrix/Diagonal.lean b/Mathlib/LinearAlgebra/Matrix/Diagonal.lean
index a8b92d3cd2a99..ff4b403c74f6f 100644
--- a/Mathlib/LinearAlgebra/Matrix/Diagonal.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Diagonal.lean
@@ -52,7 +52,7 @@ end CommSemiring
 
 section Semifield
 
-variable {m n : Type*} [Fintype m] [Fintype n] {K : Type u} [Semifield K]
+variable {m : Type*} [Fintype m] {K : Type u} [Semifield K]
 
 -- maybe try to relax the universe constraint
 theorem ker_diagonal_toLin' [DecidableEq m] (w : m → K) :
@@ -81,7 +81,7 @@ namespace LinearMap
 
 section Field
 
-variable {m n : Type*} [Fintype m] [Fintype n] {K : Type u} [Field K]
+variable {m : Type*} [Fintype m] {K : Type u} [Field K]
 
 theorem rank_diagonal [DecidableEq m] [DecidableEq K] (w : m → K) :
     LinearMap.rank (toLin' (diagonal w)) = Fintype.card { i // w i ≠ 0 } := by
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
index 0a53cfbd1d352..564c367cfcd7c 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
@@ -786,7 +786,6 @@ theorem _root_.QuadraticMap.polarBilin_injective (h : IsUnit (2 : R)) :
 section
 
 variable {N' : Type*} [AddCommGroup N'] [Module R N']
-variable [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M]
 
 theorem _root_.QuadraticMap.polarBilin_comp (Q : QuadraticMap R N' N) (f : M →ₗ[R] N') :
     polarBilin (Q.comp f) = LinearMap.compl₁₂ (polarBilin Q) f f :=
@@ -1270,7 +1269,7 @@ theorem basisRepr_apply [Fintype ι] {v : Basis ι R M} (Q : QuadraticMap R M N)
   rw [← v.equivFun_symm_apply]
   rfl
 
-variable [Fintype ι] {v : Basis ι R M}
+variable [Fintype ι]
 
 section
 
diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean
index d1a74ddcfc76d..7059fa3093f5a 100644
--- a/Mathlib/MeasureTheory/Integral/Layercake.lean
+++ b/Mathlib/MeasureTheory/Integral/Layercake.lean
@@ -458,7 +458,8 @@ end Layercake
 
 section LayercakeLT
 
-variable {α : Type*} [MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ}
+variable {α : Type*} [MeasurableSpace α]
+variable {f : α → ℝ} {g : ℝ → ℝ}
 
 /-- The layer cake formula / Cavalieri's principle / tail probability formula:
 
diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean
index 7982b328a9a8c..1bc5294a8e5f1 100644
--- a/Mathlib/RingTheory/LocalProperties/Basic.lean
+++ b/Mathlib/RingTheory/LocalProperties/Basic.lean
@@ -44,8 +44,8 @@ open scoped Pointwise Classical
 
 universe u
 
-variable {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (f : R →+* S)
-variable (N : Submonoid S) (R' S' : Type u) [CommRing R'] [CommRing S']
+variable {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
+variable (R' S' : Type u) [CommRing R'] [CommRing S']
 variable [Algebra R R'] [Algebra S S']
 
 section Properties
diff --git a/Mathlib/RingTheory/Norm/Defs.lean b/Mathlib/RingTheory/Norm/Defs.lean
index b7f2ce47f5c97..14f2d89676a6d 100644
--- a/Mathlib/RingTheory/Norm/Defs.lean
+++ b/Mathlib/RingTheory/Norm/Defs.lean
@@ -35,10 +35,9 @@ See also `Algebra.trace`, which is defined similarly as the trace of
 
 universe u v w
 
-variable {R S T : Type*} [CommRing R] [Ring S]
+variable {R S : Type*} [CommRing R] [Ring S]
 variable [Algebra R S]
-variable {K L F : Type*} [Field K] [Field L] [Field F]
-variable [Algebra K L] [Algebra K F]
+variable {K : Type*} [Field K]
 variable {ι : Type w}
 
 open Module
diff --git a/Mathlib/RingTheory/Trace/Defs.lean b/Mathlib/RingTheory/Trace/Defs.lean
index 8d961bf7c82e6..936a15a3b644d 100644
--- a/Mathlib/RingTheory/Trace/Defs.lean
+++ b/Mathlib/RingTheory/Trace/Defs.lean
@@ -42,11 +42,11 @@ For now, the definitions assume `S` is commutative, so the choice doesn't matter
 -/
 
 
-universe u v w z
+universe w
 
 variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
 variable [Algebra R S] [Algebra R T]
-variable {ι κ : Type w} [Fintype ι]
+variable {ι : Type w} [Fintype ι]
 
 open Module
 
diff --git a/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean b/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
index b9c5713bf06fd..c995eda23b8e7 100644
--- a/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
+++ b/Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
@@ -381,7 +381,7 @@ theorem toBCF_injective : Function.Injective (toBCF : C₀(α, β) → α →ᵇ
 
 end
 
-variable {C : ℝ} {f g : C₀(α, β)}
+variable {f g : C₀(α, β)}
 
 /-- The type of continuous functions vanishing at infinity, with the uniform distance induced by the
 inclusion `ZeroAtInftyContinuousMap.toBCF`, is a pseudo-metric space. -/
diff --git a/Mathlib/Topology/Instances/Matrix.lean b/Mathlib/Topology/Instances/Matrix.lean
index 3d40bfe074344..dc4f941c6159d 100644
--- a/Mathlib/Topology/Instances/Matrix.lean
+++ b/Mathlib/Topology/Instances/Matrix.lean
@@ -256,7 +256,7 @@ end Continuity
 
 section tsum
 
-variable [Semiring α] [AddCommMonoid R] [TopologicalSpace R] [Module α R]
+variable [AddCommMonoid R] [TopologicalSpace R]
 
 theorem HasSum.matrix_transpose {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) :
     HasSum (fun x => (f x)ᵀ) aᵀ :=
diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean
index 0614f4db7f848..698c804dacc7e 100644
--- a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean
+++ b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean
@@ -249,7 +249,7 @@ irreducible_def hausdorffEdist {α : Type u} [PseudoEMetricSpace α] (s t : Set
 
 section HausdorffEdist
 
-variable [PseudoEMetricSpace α] [PseudoEMetricSpace β] {x y : α} {s t u : Set α} {Φ : α → β}
+variable [PseudoEMetricSpace α] [PseudoEMetricSpace β] {x : α} {s t u : Set α} {Φ : α → β}
 
 /-- The Hausdorff edistance of a set to itself vanishes. -/
 @[simp]
diff --git a/Mathlib/Topology/MetricSpace/Thickening.lean b/Mathlib/Topology/MetricSpace/Thickening.lean
index 99f8f79bb287c..d5414b1bc048e 100644
--- a/Mathlib/Topology/MetricSpace/Thickening.lean
+++ b/Mathlib/Topology/MetricSpace/Thickening.lean
@@ -34,7 +34,7 @@ open NNReal ENNReal Topology Set Filter Bornology
 
 universe u v w
 
-variable {ι : Sort*} {α : Type u} {β : Type v}
+variable {ι : Sort*} {α : Type u}
 
 namespace Metric
 
diff --git a/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean b/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
index c4439241d6da5..c3771d10ce996 100644
--- a/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
+++ b/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
@@ -138,7 +138,7 @@ section
 attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.instFunLike
 
 variable [HasLimits C] [(forget C).ReflectsIsomorphisms] [PreservesLimits (forget C)]
-variable {X : TopCat.{v}} (F : Presheaf C X) {ι : Type v} (U : ι → Opens X)
+variable {X : TopCat.{v}} (F : Presheaf C X)
 
 /-- For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and
 preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one.