diff --git a/Mathlib/Algebra/Module/ZLattice/Covolume.lean b/Mathlib/Algebra/Module/ZLattice/Covolume.lean
index 8b3705ee2aa1e..f5740d29e7505 100644
--- a/Mathlib/Algebra/Module/ZLattice/Covolume.lean
+++ b/Mathlib/Algebra/Module/ZLattice/Covolume.lean
@@ -33,10 +33,7 @@ open Submodule MeasureTheory Module MeasureTheory Module ZSpan
 
 section General
 
-variable (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
-variable [ProperSpace E] [MeasurableSpace E]
-variable (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice K L]
+variable {E : Type*} [NormedAddCommGroup E] [ProperSpace E] [MeasurableSpace E] (L : Submodule ℤ E)
 
 /-- The covolume of a `ℤ`-lattice is the volume of some fundamental domain; see
 `ZLattice.covolume_eq_volume` for the proof that the volume does not depend on the choice of
diff --git a/Mathlib/Analysis/Calculus/Deriv/Prod.lean b/Mathlib/Analysis/Calculus/Deriv/Prod.lean
index b0640b705f958..dfd2e896128ad 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Prod.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Prod.lean
@@ -29,12 +29,7 @@ open Filter Asymptotics Set
 
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
 variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-variable {f f₀ f₁ g : 𝕜 → F}
-variable {f' f₀' f₁' g' : F}
-variable {x : 𝕜}
-variable {s t : Set 𝕜}
-variable {L L₁ L₂ : Filter 𝕜}
+variable {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {s : Set 𝕜} {L : Filter 𝕜}
 
 section CartesianProduct
 
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Pi.lean b/Mathlib/Analysis/Calculus/FDeriv/Pi.lean
index f985ae505ea08..fdc2b96749939 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Pi.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Pi.lean
@@ -11,7 +11,6 @@ import Mathlib.Analysis.Calculus.FDeriv.Add
 
 variable {𝕜 ι : Type*} [DecidableEq ι] [Fintype ι] [NontriviallyNormedField 𝕜]
 variable {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 @[fun_prop]
 theorem hasFDerivAt_update (x : ∀ i, E i) {i : ι} (y : E i) :
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Star.lean b/Mathlib/Analysis/Calculus/FDeriv/Star.lean
index 48f652a8dd13d..933c9c2c4fdc1 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Star.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Star.lean
@@ -27,7 +27,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type*} [NormedAddCommGroup F] [StarAddMonoid F] [NormedSpace 𝕜 F] [StarModule 𝕜 F]
   [ContinuousStar F]
 
-variable {f : E → F} {f' : E →L[𝕜] F} (e : E →L[𝕜] F) {x : E} {s : Set E} {L : Filter E}
+variable {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} {L : Filter E}
 
 @[fun_prop]
 theorem HasStrictFDerivAt.star (h : HasStrictFDerivAt f f' x) :
diff --git a/Mathlib/Analysis/Calculus/Gradient/Basic.lean b/Mathlib/Analysis/Calculus/Gradient/Basic.lean
index 558b091cb21ac..5ebf3d941d6a8 100644
--- a/Mathlib/Analysis/Calculus/Gradient/Basic.lean
+++ b/Mathlib/Analysis/Calculus/Gradient/Basic.lean
@@ -252,7 +252,7 @@ section congr
 
 /-! ### Congruence properties of the Gradient -/
 
-variable {f₀ f₁ : F → 𝕜} {f₀' f₁' : F} {x₀ x₁ : F} {s₀ s₁ t : Set F} {L₀ L₁ : Filter F}
+variable {f₀ f₁ : F → 𝕜} {f₀' f₁' : F} {t : Set F}
 
 theorem Filter.EventuallyEq.hasGradientAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x)
     (h₁ : f₀' = f₁') : HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L :=
diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
index 67b3db1e4cd80..b23236aaf0baf 100644
--- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
+++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
@@ -52,8 +52,6 @@ noncomputable section
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
-variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
 variable {ε : ℝ}
 
 open Filter Metric Set
diff --git a/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean b/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
index 3de1ac70f4558..b675314ee9710 100644
--- a/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
@@ -475,7 +475,7 @@ section CompRight
 
 variable {E : Type*} [AddCommGroup E] [Module 𝕜 E]
   {E' : Type*} [AddCommGroup E'] [Module 𝕜 E']
-  {f : E → F} {f' : F} {x v : E'} {L : E' →ₗ[𝕜] E}
+  {f : E → F} {f' : F} {x : E'} {L : E' →ₗ[𝕜] E}
 
 theorem HasLineDerivAt.of_comp {v : E'} (hf : HasLineDerivAt 𝕜 (f ∘ L) f' x v) :
     HasLineDerivAt 𝕜 f f' (L x) (L v) := by
diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
index 6376b28c74713..49b3978cb0252 100644
--- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
@@ -66,7 +66,7 @@ variable [MeasurableSpace X]
 section NormedAddCommGroup
 
 variable [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f g : X → E} {s t : Set X} {μ ν : Measure X} {l l' : Filter X}
+  {f g : X → E} {s t : Set X} {μ : Measure X}
 
 theorem setIntegral_congr_ae₀ (hs : NullMeasurableSet s μ) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
     ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ :=
diff --git a/Mathlib/Order/PrimeIdeal.lean b/Mathlib/Order/PrimeIdeal.lean
index e8b6364e05f7b..aef2ade7bdfd4 100644
--- a/Mathlib/Order/PrimeIdeal.lean
+++ b/Mathlib/Order/PrimeIdeal.lean
@@ -101,7 +101,7 @@ end Preorder
 
 section SemilatticeInf
 
-variable [SemilatticeInf P] {x y : P} {I : Ideal P}
+variable [SemilatticeInf P] {I : Ideal P}
 
 theorem IsPrime.mem_or_mem (hI : IsPrime I) {x y : P} : x ⊓ y ∈ I → x ∈ I ∨ y ∈ I := by
   contrapose!
diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean
index 43f54dab8c27d..77f3a13bb4a8c 100644
--- a/Mathlib/Probability/Distributions/Uniform.lean
+++ b/Mathlib/Probability/Distributions/Uniform.lean
@@ -48,7 +48,7 @@ noncomputable section
 
 namespace MeasureTheory
 
-variable {E : Type*} [MeasurableSpace E] {m : Measure E} {μ : Measure E}
+variable {E : Type*} [MeasurableSpace E] {μ : Measure E}
 
 namespace pdf
 
@@ -206,7 +206,7 @@ end MeasureTheory
 
 namespace PMF
 
-variable {α β γ : Type*}
+variable {α : Type*}
 
 open scoped Classical NNReal ENNReal
 
diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean
index 9a2db5e2be4bc..5dbebd1c9f25c 100644
--- a/Mathlib/Probability/Kernel/Composition.lean
+++ b/Mathlib/Probability/Kernel/Composition.lean
@@ -65,7 +65,7 @@ namespace ProbabilityTheory
 
 namespace Kernel
 
-variable {α β ι : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
 
 section CompositionProduct
 
@@ -335,7 +335,7 @@ end Ae
 
 section Restrict
 
-variable {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {a : α}
+variable {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η]
 
 theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
     Kernel.restrict κ hs ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (hs.prod ht) := by
@@ -759,7 +759,7 @@ def prodMkLeft (γ : Type*) [MeasurableSpace γ] (κ : Kernel α β) : Kernel (
 def prodMkRight (γ : Type*) [MeasurableSpace γ] (κ : Kernel α β) : Kernel (α × γ) β :=
   comap κ Prod.fst measurable_fst
 
-variable {γ : Type*} {mγ : MeasurableSpace γ} {f : β → γ} {g : γ → α}
+variable {γ : Type*} {mγ : MeasurableSpace γ}
 
 @[simp]
 theorem prodMkLeft_apply (κ : Kernel α β) (ca : γ × α) : prodMkLeft γ κ ca = κ ca.snd :=
diff --git a/Mathlib/Probability/Kernel/Disintegration/CondCDF.lean b/Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
index a5c415461bb5b..c02e122e3cff2 100644
--- a/Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
+++ b/Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
@@ -42,7 +42,7 @@ open scoped NNReal ENNReal MeasureTheory Topology
 
 namespace MeasureTheory.Measure
 
-variable {α β : Type*} {mα : MeasurableSpace α} (ρ : Measure (α × ℝ))
+variable {α : Type*} {mα : MeasurableSpace α} (ρ : Measure (α × ℝ))
 
 /-- Measure on `α` such that for a measurable set `s`, `ρ.IicSnd r s = ρ (s ×ˢ Iic r)`. -/
 noncomputable def IicSnd (r : ℝ) : Measure α :=
@@ -112,7 +112,7 @@ open MeasureTheory
 
 namespace ProbabilityTheory
 
-variable {α β ι : Type*} {mα : MeasurableSpace α}
+variable {α : Type*} {mα : MeasurableSpace α}
 
 attribute [local instance] MeasureTheory.Measure.IsFiniteMeasure.IicSnd
 
diff --git a/Mathlib/Probability/Kernel/Integral.lean b/Mathlib/Probability/Kernel/Integral.lean
index f259203acbe03..e97ef25407719 100644
--- a/Mathlib/Probability/Kernel/Integral.lean
+++ b/Mathlib/Probability/Kernel/Integral.lean
@@ -91,7 +91,7 @@ end Const
 
 section Restrict
 
-variable {s t : Set β}
+variable {s : Set β}
 
 @[simp]
 theorem integral_restrict (hs : MeasurableSet s) :
diff --git a/Mathlib/Probability/Kernel/Invariance.lean b/Mathlib/Probability/Kernel/Invariance.lean
index 58d1a2185d16b..e9d40e85a0dd9 100644
--- a/Mathlib/Probability/Kernel/Invariance.lean
+++ b/Mathlib/Probability/Kernel/Invariance.lean
@@ -30,7 +30,7 @@ open scoped MeasureTheory ENNReal ProbabilityTheory
 
 namespace ProbabilityTheory
 
-variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
 
 namespace Kernel
 
diff --git a/Mathlib/Probability/Kernel/MeasurableIntegral.lean b/Mathlib/Probability/Kernel/MeasurableIntegral.lean
index 2d5fff10ca258..63c99fb77ebfa 100644
--- a/Mathlib/Probability/Kernel/MeasurableIntegral.lean
+++ b/Mathlib/Probability/Kernel/MeasurableIntegral.lean
@@ -231,7 +231,7 @@ alias _root_.Measurable.set_lintegral_kernel := _root_.Measurable.setLIntegral_k
 
 end Lintegral
 
-variable {E : Type*} [NormedAddCommGroup E] [IsSFiniteKernel κ] [IsSFiniteKernel η]
+variable {E : Type*} [NormedAddCommGroup E] [IsSFiniteKernel κ]
 
 theorem measurableSet_kernel_integrable ⦃f : α → β → E⦄ (hf : StronglyMeasurable (uncurry f)) :
     MeasurableSet {x | Integrable (f x) (κ x)} := by
diff --git a/Mathlib/Probability/Martingale/OptionalSampling.lean b/Mathlib/Probability/Martingale/OptionalSampling.lean
index 535963b759aba..90b9489aaa39c 100644
--- a/Mathlib/Probability/Martingale/OptionalSampling.lean
+++ b/Mathlib/Probability/Martingale/OptionalSampling.lean
@@ -143,11 +143,11 @@ and is a measurable space with the Borel σ-algebra. -/
 
 variable {ι : Type*} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [TopologicalSpace ι]
   [DiscreteTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasurableSpace E] [BorelSpace E]
-  [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → ι} {f : ι → Ω → E} {i n : ι}
+  [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → ι} {f : ι → Ω → E} {i : ι}
 
 theorem condexp_stoppedValue_stopping_time_ae_eq_restrict_le (h : Martingale f ℱ μ)
     (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim hσ.measurableSpace_le)]
-    (hτ_le : ∀ x, τ x ≤ n) :
+    (hτ_le : ∀ x, τ x ≤ i) :
     μ[stoppedValue f τ|hσ.measurableSpace] =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] stoppedValue f τ := by
   rw [ae_eq_restrict_iff_indicator_ae_eq
     (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))]
diff --git a/Mathlib/RingTheory/Flat/Stability.lean b/Mathlib/RingTheory/Flat/Stability.lean
index 57de113408f23..8b0e1c14b0fa9 100644
--- a/Mathlib/RingTheory/Flat/Stability.lean
+++ b/Mathlib/RingTheory/Flat/Stability.lean
@@ -153,7 +153,7 @@ section Localization
 
 variable {R : Type u} {M Mp : Type*} (Rp : Type v)
   [CommRing R] [AddCommGroup M] [Module R M] [CommRing Rp] [Algebra R Rp]
-  [AddCommGroup Mp] [Module R Mp] [Module Rp Mp] [IsScalarTower R Rp Mp] (f : M →ₗ[R] Mp)
+  [AddCommGroup Mp] [Module R Mp] [Module Rp Mp] [IsScalarTower R Rp Mp]
 
 instance localizedModule [Module.Flat R M] (S : Submonoid R) : Module.Flat (Localization S)
     (LocalizedModule S M) := by
diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
index b4e933391ff50..c3b6bf05ac681 100644
--- a/Mathlib/RingTheory/HahnSeries/Summable.lean
+++ b/Mathlib/RingTheory/HahnSeries/Summable.lean
@@ -42,7 +42,7 @@ open Pointwise
 
 noncomputable section
 
-variable {Γ Γ' R V α β : Type*}
+variable {Γ R α β : Type*}
 
 namespace HahnSeries
 
diff --git a/Mathlib/RingTheory/LocalRing/Module.lean b/Mathlib/RingTheory/LocalRing/Module.lean
index 332bccee7c8f5..d446db6698308 100644
--- a/Mathlib/RingTheory/LocalRing/Module.lean
+++ b/Mathlib/RingTheory/LocalRing/Module.lean
@@ -28,7 +28,7 @@ This file gathers various results about finite modules over a local ring `(R, 
   `l` is a split injection if and only if `k ⊗ l` is a (split) injection.
 -/
 
-variable {R S} [CommRing R] [CommRing S] [Algebra R S]
+variable {R} [CommRing R]
 
 section
 
diff --git a/Mathlib/RingTheory/Regular/IsSMulRegular.lean b/Mathlib/RingTheory/Regular/IsSMulRegular.lean
index efe4d52d7cef9..3619263bfda72 100644
--- a/Mathlib/RingTheory/Regular/IsSMulRegular.lean
+++ b/Mathlib/RingTheory/Regular/IsSMulRegular.lean
@@ -136,7 +136,7 @@ open Submodule Pointwise
 
 variable (M) [CommRing R] [AddCommGroup M] [Module R M]
     [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M'']
-    (I : Ideal R) (N : Submodule R M) (r : R)
+    (N : Submodule R M) (r : R)
 
 variable (R) in
 lemma biUnion_associatedPrimes_eq_compl_regular [IsNoetherianRing R] :
diff --git a/Mathlib/Topology/Order/UpperLowerSetTopology.lean b/Mathlib/Topology/Order/UpperLowerSetTopology.lean
index 02681dbd9f86d..c3e5e3a52ad12 100644
--- a/Mathlib/Topology/Order/UpperLowerSetTopology.lean
+++ b/Mathlib/Topology/Order/UpperLowerSetTopology.lean
@@ -95,7 +95,7 @@ protected def rec {β : WithUpperSet α → Sort*} (h : ∀ a, β (toUpperSet a)
 instance [Nonempty α] : Nonempty (WithUpperSet α) := ‹Nonempty α›
 instance [Inhabited α] : Inhabited (WithUpperSet α) := ‹Inhabited α›
 
-variable [Preorder α] [Preorder β] [Preorder γ]
+variable [Preorder α] [Preorder β]
 
 instance : Preorder (WithUpperSet α) := ‹Preorder α›
 instance : TopologicalSpace (WithUpperSet α) := upperSet α