diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean
index b6445fadfe529..594d62bba3e1d 100644
--- a/Mathlib/LinearAlgebra/Dimension/Localization.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean
@@ -120,7 +120,7 @@ end CommRing
 
 section Ring
 
-variable {R} [Ring R] [IsDomain R] (S : Submonoid R)
+variable {R} [Ring R] [IsDomain R]
 
 /-- A domain that is not (left) Ore is of infinite rank.
 See [cohn_1995] Proposition 1.3.6 -/
diff --git a/Mathlib/LinearAlgebra/Matrix/Circulant.lean b/Mathlib/LinearAlgebra/Matrix/Circulant.lean
index c81affc351505..2e87e67a1fa42 100644
--- a/Mathlib/LinearAlgebra/Matrix/Circulant.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Circulant.lean
@@ -32,7 +32,7 @@ circulant, matrix
 -/
 
 
-variable {α β m n R : Type*}
+variable {α β n R : Type*}
 
 namespace Matrix
 
diff --git a/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean b/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
index b339fa3a131cc..ae27ada2167b0 100644
--- a/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
@@ -25,7 +25,7 @@ open Set Function Module
 
 noncomputable section
 
-variable {ι R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
 
 namespace LinearMap
 
diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
index 83a31d388715d..133145051b3f2 100644
--- a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
+++ b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
@@ -88,7 +88,7 @@ lemma rnDeriv_pos' [HaveLebesgueDecomposition ν μ] [SigmaFinite μ] (hμν : 
 
 section rnDeriv_withDensity_leftRight
 
-variable {μ ν : Measure α} {f : α → ℝ≥0∞}
+variable {f : α → ℝ≥0∞}
 
 /-- Auxiliary lemma for `rnDeriv_withDensity_left`. -/
 lemma rnDeriv_withDensity_withDensity_rnDeriv_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
diff --git a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
index a74a832aa9956..7652993309eaf 100644
--- a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
+++ b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
@@ -46,7 +46,7 @@ open scoped Classical MeasureTheory NNReal ENNReal
 
 open Set
 
-variable {α β : Type*} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
+variable {α : Type*} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
 
 namespace MeasureTheory
 
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
index bf52c95cfaeaa..95319082eb996 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
@@ -175,12 +175,10 @@ theorem AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on {α
     hf_ind.stronglyMeasurable_of_measurableSpace_le_on hs_m hs fun x hxs =>
       Set.indicator_of_not_mem hxs _
 
-variable {α F F' 𝕜 : Type*} {p : ℝ≥0∞} [RCLike 𝕜]
+variable {α F 𝕜 : Type*} {p : ℝ≥0∞} [RCLike 𝕜]
   -- 𝕜 for ℝ or ℂ
   -- F for a Lp submodule
   [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-  -- F' for integrals on a Lp submodule
-  [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F']
 
 section LpMeas
 
diff --git a/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean b/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean
index 674e34c9ca6f3..095d95dd608a0 100644
--- a/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean
@@ -26,13 +26,13 @@ noncomputable section
 
 open scoped MeasureTheory NNReal ENNReal
 
-variable {α β : Type*} {m : MeasurableSpace α}
+variable {α : Type*} {m : MeasurableSpace α}
 
 namespace MeasureTheory
 
 open TopologicalSpace
 
-variable {μ ν : Measure α}
+variable {μ : Measure α}
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 open Classical in
diff --git a/Mathlib/ModelTheory/Graph.lean b/Mathlib/ModelTheory/Graph.lean
index c4ce433290e9c..ed3a509c17c55 100644
--- a/Mathlib/ModelTheory/Graph.lean
+++ b/Mathlib/ModelTheory/Graph.lean
@@ -21,7 +21,7 @@ This file defines first-order languages, structures, and theories in graph theor
   of the theory of simple graphs.
 -/
 
-universe u v
+universe u
 
 namespace FirstOrder
 
@@ -31,7 +31,7 @@ open FirstOrder
 
 open Structure
 
-variable {α : Type u} {V : Type v} {n : ℕ}
+variable {V : Type u} {n : ℕ}
 
 /-! ### Simple Graphs -/
 
diff --git a/Mathlib/ModelTheory/PartialEquiv.lean b/Mathlib/ModelTheory/PartialEquiv.lean
index 3db2f33308397..49e73c8f359f2 100644
--- a/Mathlib/ModelTheory/PartialEquiv.lean
+++ b/Mathlib/ModelTheory/PartialEquiv.lean
@@ -40,8 +40,8 @@ namespace FirstOrder
 
 namespace Language
 
-variable (L : Language.{u, v}) (M : Type w) (N : Type w') {P : Type*}
-variable [L.Structure M] [L.Structure N] [L.Structure P]
+variable (L : Language.{u, v}) (M : Type w) (N : Type w')
+variable [L.Structure M] [L.Structure N]
 
 open FirstOrder Structure Substructure
 
diff --git a/Mathlib/NumberTheory/Cyclotomic/Gal.lean b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
index fb381459d36cf..c5f27c52696f2 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Gal.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
@@ -152,7 +152,7 @@ end IsCyclotomicExtension
 
 section Gal
 
-variable [Field L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L]
+variable [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L]
   (h : Irreducible (cyclotomic n K)) {K}
 
 /-- `IsCyclotomicExtension.autEquivPow` repackaged in terms of `Gal`.
diff --git a/Mathlib/NumberTheory/Dioph.lean b/Mathlib/NumberTheory/Dioph.lean
index 721b81b5271ba..6c7c378d55eb4 100644
--- a/Mathlib/NumberTheory/Dioph.lean
+++ b/Mathlib/NumberTheory/Dioph.lean
@@ -67,7 +67,7 @@ Note that this duplicates `MvPolynomial`.
 
 section Polynomials
 
-variable {α β γ : Type*}
+variable {α β : Type*}
 
 /-- A predicate asserting that a function is a multivariate integer polynomial.
   (We are being a bit lazy here by allowing many representations for multiplication,
@@ -432,7 +432,7 @@ end
 
 section
 
-variable {α β : Type} {n : ℕ}
+variable {α : Type} {n : ℕ}
 
 open Vector3
 
diff --git a/Mathlib/Order/Ideal.lean b/Mathlib/Order/Ideal.lean
index 4dae232039074..7c8fe0e4ef08f 100644
--- a/Mathlib/Order/Ideal.lean
+++ b/Mathlib/Order/Ideal.lean
@@ -92,7 +92,7 @@ variable [LE P]
 
 section
 
-variable {I J s t : Ideal P} {x y : P}
+variable {I s t : Ideal P} {x : P}
 
 theorem toLowerSet_injective : Injective (toLowerSet : Ideal P → LowerSet P) := fun s t _ ↦ by
   cases s
@@ -247,7 +247,7 @@ variable [Preorder P]
 
 section
 
-variable {I J : Ideal P} {x y : P}
+variable {I : Ideal P} {x y : P}
 
 /-- The smallest ideal containing a given element. -/
 @[simps]
@@ -316,7 +316,7 @@ end SemilatticeSup
 
 section SemilatticeSupDirected
 
-variable [SemilatticeSup P] [IsDirected P (· ≥ ·)] {x : P} {I J K s t : Ideal P}
+variable [SemilatticeSup P] [IsDirected P (· ≥ ·)] {x : P} {I J s t : Ideal P}
 
 /-- The infimum of two ideals of a co-directed order is their intersection. -/
 instance : Inf (Ideal P) :=
@@ -385,7 +385,7 @@ end SemilatticeSupDirected
 
 section SemilatticeSupOrderBot
 
-variable [SemilatticeSup P] [OrderBot P] {x : P} {I J K : Ideal P}
+variable [SemilatticeSup P] [OrderBot P] {x : P}
 
 instance : InfSet (Ideal P) :=
   ⟨fun S ↦
diff --git a/Mathlib/RingTheory/DedekindDomain/Dvr.lean b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
index 2edc66bfc7bfa..c7086a988650b 100644
--- a/Mathlib/RingTheory/DedekindDomain/Dvr.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
@@ -43,7 +43,7 @@ dedekind domain, dedekind ring
 -/
 
 
-variable (R A K : Type*) [CommRing R] [CommRing A] [IsDomain A] [Field K]
+variable (A : Type*) [CommRing A] [IsDomain A]
 
 open scoped nonZeroDivisors Polynomial
 
diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
index 5957f090f0b89..763ee85bc69d5 100644
--- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
+++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
@@ -25,7 +25,7 @@ Also see `tfae_of_isNoetherianRing_of_localRing_of_isDomain` for a version witho
 -/
 
 
-variable (R : Type*) [CommRing R] (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
+variable (R : Type*) [CommRing R]
 
 open scoped Multiplicative
 
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
index 65b589c7373de..8965ee6ddf242 100644
--- a/Mathlib/RingTheory/PowerSeries/Basic.lean
+++ b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -758,7 +758,7 @@ namespace Polynomial
 
 open Finsupp Polynomial
 
-variable {σ : Type*} {R : Type*} [CommSemiring R] (φ ψ : R[X])
+variable {R : Type*} [CommSemiring R] (φ ψ : R[X])
 
 -- Porting note: added so we can add the `@[coe]` attribute
 /-- The natural inclusion from polynomials into formal power series. -/
diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean
index 18c6913c525cd..660923cc4da32 100644
--- a/Mathlib/RingTheory/PowerSeries/Inverse.lean
+++ b/Mathlib/RingTheory/PowerSeries/Inverse.lean
@@ -274,7 +274,7 @@ theorem map.isLocalHom : IsLocalHom (map f) :=
 @[deprecated (since := "2024-10-10")]
 alias map.isLocalRingHom := map.isLocalHom
 
-variable [LocalRing R] [LocalRing S]
+variable [LocalRing R]
 
 instance : LocalRing R⟦X⟧ :=
   { inferInstanceAs <| LocalRing <| MvPowerSeries Unit R with }