diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
index 9472500e7fcc9..404fdd46e25ad 100644
--- a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@@ -38,7 +38,7 @@ lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
 end Mul
 
 section InvolutiveInv
-variable [InvolutiveInv G] {s t : Set G}
+variable [InvolutiveInv G]
 
 @[to_additive (attr := simp)]
 lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by
diff --git a/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean b/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean
index 8466c8876f1c1..4e144b113a816 100644
--- a/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean
+++ b/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean
@@ -13,7 +13,7 @@ import Mathlib.SetTheory.Cardinal.Finite
 
 open scoped Cardinal Pointwise
 
-variable {G G₀ M M₀ : Type*}
+variable {G₀ M₀ : Type*}
 
 namespace Set
 variable [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀}
diff --git a/Mathlib/Algebra/Homology/Additive.lean b/Mathlib/Algebra/Homology/Additive.lean
index 5fbebb2c8beb9..1b14c45bf5b00 100644
--- a/Mathlib/Algebra/Homology/Additive.lean
+++ b/Mathlib/Algebra/Homology/Additive.lean
@@ -23,8 +23,8 @@ variable {ι : Type*}
 variable {V : Type u} [Category.{v} V] [Preadditive V]
 variable {W : Type*} [Category W] [Preadditive W]
 variable {W₁ W₂ : Type*} [Category W₁] [Category W₂] [HasZeroMorphisms W₁] [HasZeroMorphisms W₂]
-variable {c : ComplexShape ι} {C D E : HomologicalComplex V c}
-variable (f g : C ⟶ D) (h k : D ⟶ E) (i : ι)
+variable {c : ComplexShape ι} {C D : HomologicalComplex V c}
+variable (f : C ⟶ D) (i : ι)
 
 namespace HomologicalComplex
 
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index 69ce497aff36a..1ee91c3592cc2 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/Mathlib/Algebra/Quaternion.lean
@@ -93,7 +93,7 @@ theorem equivTuple_apply {R : Type*} (c₁ c₂ : R) (x : ℍ[R,c₁,c₂]) :
 @[simp]
 theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a.4 = a := rfl
 
-variable {S T R : Type*} {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂])
+variable {S T R : Type*} {c₁ c₂ : R} (r x y : R) (a b : ℍ[R,c₁,c₂])
 
 instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton
 instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial
@@ -742,7 +742,7 @@ instance {R : Type*} [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R] :=
 
 namespace Quaternion
 
-variable {S T R : Type*} [CommRing R] (r x y z : R) (a b c : ℍ[R])
+variable {S T R : Type*} [CommRing R] (r x y : R) (a b : ℍ[R])
 
 export QuaternionAlgebra (re imI imJ imK)
 
diff --git a/Mathlib/Algebra/TrivSqZeroExt.lean b/Mathlib/Algebra/TrivSqZeroExt.lean
index c40ab975c18d7..cc4239ab85e25 100644
--- a/Mathlib/Algebra/TrivSqZeroExt.lean
+++ b/Mathlib/Algebra/TrivSqZeroExt.lean
@@ -870,10 +870,9 @@ section Algebra
 
 variable (S : Type*) (R R' : Type u) (M : Type v)
 variable [CommSemiring S] [Semiring R] [CommSemiring R'] [AddCommMonoid M]
-variable [Algebra S R] [Algebra S R'] [Module S M]
-variable [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+variable [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
 variable [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M]
-variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] [IsScalarTower S R' M]
+variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]
 
 instance algebra' : Algebra S (tsze R M) :=
   { (TrivSqZeroExt.inlHom R M).comp (algebraMap S R) with
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
index 51f9c3ccf41d9..070c60d31cc77 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@@ -142,8 +142,7 @@ instance inf (P Q : MorphismProperty Scheme) [IsLocalAtTarget P] [IsLocalAtTarge
      fun h ↦ ⟨(iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).left),
       (iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).right)⟩⟩
 
-variable {P} [hP : IsLocalAtTarget P]
-variable {X Y U V : Scheme.{u}} {f : X ⟶ Y} {g : U ⟶ Y} [IsOpenImmersion g] (𝒰 : Y.OpenCover)
+variable {P} [hP : IsLocalAtTarget P] {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : Y.OpenCover)
 
 lemma of_isPullback {UX UY : Scheme.{u}} {iY : UY ⟶ Y} [IsOpenImmersion iY]
     {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : IsPullback iX f' f iY) (H : P f) : P f' := by
@@ -228,7 +227,7 @@ instance inf (P Q : MorphismProperty Scheme) [IsLocalAtSource P] [IsLocalAtSourc
       (iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).right)⟩⟩
 
 variable {P} [IsLocalAtSource P]
-variable {X Y U V : Scheme.{u}} {f : X ⟶ Y} {g : U ⟶ Y} [IsOpenImmersion g] (𝒰 : X.OpenCover)
+variable {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : X.OpenCover)
 
 lemma comp {UX : Scheme.{u}} (H : P f) (i : UX ⟶ X) [IsOpenImmersion i] :
     P (i ≫ f) :=
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean b/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean
index 665513b4b09cb..35ee3280f7055 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean
@@ -28,7 +28,7 @@ abbrev IsEtale {X Y : Scheme.{u}} (f : X ⟶ Y) := IsSmoothOfRelativeDimension 0
 
 namespace IsEtale
 
-variable {X Y : Scheme.{u}} (f : X ⟶ Y)
+variable {X : Scheme.{u}}
 
 instance : IsStableUnderBaseChange @IsEtale :=
   isSmoothOfRelativeDimension_isStableUnderBaseChange 0
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
index 880a1a62832f1..6cd62e8973f1b 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
@@ -26,7 +26,7 @@ universe u
 
 namespace AlgebraicGeometry
 
-variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
+variable {X Y : Scheme.{u}}
 
 theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} : IsOpenImmersion f ↔
     IsOpenEmbedding f.base ∧ ∀ x, IsIso (f.stalkMap x) := by
diff --git a/Mathlib/AlgebraicGeometry/SpreadingOut.lean b/Mathlib/AlgebraicGeometry/SpreadingOut.lean
index b5d7ef83b97b8..a327e1ae7ee02 100644
--- a/Mathlib/AlgebraicGeometry/SpreadingOut.lean
+++ b/Mathlib/AlgebraicGeometry/SpreadingOut.lean
@@ -49,8 +49,7 @@ open CategoryTheory
 
 namespace AlgebraicGeometry
 
-variable {X Y S : Scheme.{u}} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (e : f ≫ sY = sX)
-variable {R A : CommRingCat.{u}}
+variable {X Y S : Scheme.{u}} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) {R A : CommRingCat.{u}}
 
 /-- The germ map at `x` is injective if there exists some affine `U ∋ x`
   such that the map `Γ(X, U) ⟶ X_x` is injective -/
diff --git a/Mathlib/Analysis/Convex/Gauge.lean b/Mathlib/Analysis/Convex/Gauge.lean
index 5ecb5e8b2c4cd..f9d037d23877a 100644
--- a/Mathlib/Analysis/Convex/Gauge.lean
+++ b/Mathlib/Analysis/Convex/Gauge.lean
@@ -41,7 +41,7 @@ open scoped Pointwise Topology NNReal
 
 noncomputable section
 
-variable {𝕜 E F : Type*}
+variable {𝕜 E : Type*}
 
 section AddCommGroup
 
diff --git a/Mathlib/Analysis/Convex/Normed.lean b/Mathlib/Analysis/Convex/Normed.lean
index fae3e58b55f18..9a305c1457de0 100644
--- a/Mathlib/Analysis/Convex/Normed.lean
+++ b/Mathlib/Analysis/Convex/Normed.lean
@@ -25,14 +25,14 @@ We prove the following facts:
   is bounded.
 -/
 
-variable {ι : Type*} {E P : Type*}
+variable {E P : Type*}
 
 open AffineBasis Module Metric Set
 open scoped Convex Pointwise Topology
 
 section SeminormedAddCommGroup
 variable [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P]
-variable {s t : Set E}
+variable {s : Set E}
 
 /-- The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn`
 and `convexOn_univ_norm`. -/
diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
index 2f715eb17ed19..6f06b27cb078c 100644
--- a/Mathlib/Analysis/InnerProductSpace/Basic.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -1600,9 +1600,7 @@ end ContinuousLinearMap
 
 section
 
-variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
-variable {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
-variable {E'' : Type*} [SeminormedAddCommGroup E''] [InnerProductSpace 𝕜 E'']
+variable {ι : Type*} {ι' : Type*} {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
 
 @[simp]
 theorem Orthonormal.equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
@@ -1683,7 +1681,7 @@ open scoped InnerProductSpace
 
 variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
-variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
+variable {ι : Type*}
 
 local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 
@@ -2188,9 +2186,7 @@ local notation "IK" => @RCLike.I 𝕜 _
 
 local postfix:90 "†" => starRingEnd _
 
-variable {ι : Type*}
-variable {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)] [∀ i, InnerProductSpace 𝕜 (G i)]
-  {V : ∀ i, G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [dec_V : ∀ (i) (x : G i), Decidable (x ≠ 0)]
+variable {ι : Type*} {G : ι → Type*}
 
 /-- An orthogonal family forms an independent family of subspaces; that is, any collection of
 elements each from a different subspace in the family is linearly independent. In particular, the
diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean
index eb3c22b61051f..00424d49f8973 100644
--- a/Mathlib/Analysis/Normed/Field/Basic.lean
+++ b/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -955,7 +955,7 @@ theorem NormedAddCommGroup.tendsto_atTop' [Nonempty α] [Preorder α] [IsDirecte
 
 section RingHomIsometric
 
-variable {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
+variable {R₁ R₂ : Type*}
 
 /-- This class states that a ring homomorphism is isometric. This is a sufficient assumption
 for a continuous semilinear map to be bounded and this is the main use for this typeclass. -/
@@ -965,7 +965,7 @@ class RingHomIsometric [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (
 
 attribute [simp] RingHomIsometric.is_iso
 
-variable [SeminormedRing R₁] [SeminormedRing R₂] [SeminormedRing R₃]
+variable [SeminormedRing R₁]
 
 instance RingHomIsometric.ids : RingHomIsometric (RingHom.id R₁) :=
   ⟨rfl⟩
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index 91cdbe19d79a5..dd3bf2a5b2797 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -44,7 +44,7 @@ normed group
 -/
 
 
-variable {𝓕 𝕜 α ι κ E F G : Type*}
+variable {𝓕 α ι κ E F G : Type*}
 
 open Filter Function Metric Bornology
 
@@ -337,7 +337,7 @@ abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommG
 section SeminormedGroup
 
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b b₁ b₂ c : E} {r r₁ r₂ : ℝ}
+  {a a₁ a₂ b c : E} {r r₁ r₂ : ℝ}
 
 @[to_additive]
 theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ :=
@@ -1024,7 +1024,7 @@ end Induced
 
 section SeminormedCommGroup
 
-variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a b : E} {r : ℝ}
 
 @[to_additive]
 theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹ := by
@@ -1290,7 +1290,7 @@ end SeminormedCommGroup
 
 section NormedGroup
 
-variable [NormedGroup E] [NormedGroup F] {a b : E}
+variable [NormedGroup E] {a b : E}
 
 @[to_additive (attr := simp) norm_eq_zero]
 theorem norm_eq_zero'' : ‖a‖ = 0 ↔ a = 1 :=
diff --git a/Mathlib/Analysis/Normed/Group/Bounded.lean b/Mathlib/Analysis/Normed/Group/Bounded.lean
index bd28a0b52f340..dcebdaec8bfb2 100644
--- a/Mathlib/Analysis/Normed/Group/Bounded.lean
+++ b/Mathlib/Analysis/Normed/Group/Bounded.lean
@@ -21,11 +21,10 @@ normed group
 open Filter Metric Bornology
 open scoped Pointwise Topology
 
-variable {α ι E F G : Type*}
+variable {α E F G : Type*}
 
 section SeminormedGroup
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
 
 @[to_additive (attr := simp) comap_norm_atTop]
 lemma comap_norm_atTop' : comap norm atTop = cobounded E := by
diff --git a/Mathlib/Analysis/Normed/Group/Uniform.lean b/Mathlib/Analysis/Normed/Group/Uniform.lean
index 8f4a7f9f06b4e..73b33458e9210 100644
--- a/Mathlib/Analysis/Normed/Group/Uniform.lean
+++ b/Mathlib/Analysis/Normed/Group/Uniform.lean
@@ -15,13 +15,13 @@ This file proves lipschitzness of normed group operations and shows that normed
 groups.
 -/
 
-variable {𝓕 α E F : Type*}
+variable {𝓕 E F : Type*}
 
 open Filter Function Metric Bornology
 open scoped ENNReal NNReal Uniformity Pointwise Topology
 
 section SeminormedGroup
-variable [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a b : E} {r : ℝ}
 
 @[to_additive]
 instance NormedGroup.to_isometricSMul_right : IsometricSMul Eᵐᵒᵖ E :=
@@ -177,7 +177,7 @@ end SeminormedGroup
 
 section SeminormedCommGroup
 
-variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ}
 
 @[to_additive]
 instance NormedGroup.to_isometricSMul_left : IsometricSMul E E :=
@@ -239,7 +239,7 @@ theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
 
 section PseudoEMetricSpace
 variable {α E : Type*} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0}
-  {f g : α → E} {s : Set α} {x : α}
+  {f g : α → E} {s : Set α}
 
 @[to_additive (attr := simp)]
 lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith]
diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
index 303247548cea2..789c690f2042f 100644
--- a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
+++ b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -54,8 +54,7 @@ namespace LinearIsometry
 
 open LinearMap
 
-variable {R : Type*} [Semiring R]
-variable {F E₁ : Type*} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] [Module R E₁]
+variable {F E₁ : Type*} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁]
 variable {R₁ : Type*} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁]
   [FiniteDimensional R₁ F]
 
@@ -110,9 +109,7 @@ end AffineIsometry
 section CompleteField
 
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type x}
-  [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F']
-  [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜]
+  [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜]
 
 section Affine
 
diff --git a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean
index d11a3d4ac62c1..ffb59cad14a86 100644
--- a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean
@@ -22,7 +22,6 @@ open CategoryTheory.Limits
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-  (E : Type u₃) [Category.{v₃} E]
 
 noncomputable section
 
diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean
index b6e2df434c2b9..2bc160aeba95d 100644
--- a/Mathlib/CategoryTheory/GradedObject.lean
+++ b/Mathlib/CategoryTheory/GradedObject.lean
@@ -316,7 +316,7 @@ lemma hasMap_of_iso (e : X ≅ Y) (p: I → J) [HasMap X p] : HasMap Y p := fun
   exact hasColimitOfIso α.symm
 
 section
-variable [X.HasMap p] [Y.HasMap p] [Z.HasMap p]
+variable [X.HasMap p] [Y.HasMap p]
 
 /-- Given `X : GradedObject I C` and `p : I → J`, `X.mapObj p` is the graded object by `J`
 which in degree `j` consists of the coproduct of the `X i` such that `p i = j`. -/
diff --git a/Mathlib/CategoryTheory/GuitartExact/Basic.lean b/Mathlib/CategoryTheory/GuitartExact/Basic.lean
index cb64500850d99..b697c1ee0f1a1 100644
--- a/Mathlib/CategoryTheory/GuitartExact/Basic.lean
+++ b/Mathlib/CategoryTheory/GuitartExact/Basic.lean
@@ -128,7 +128,6 @@ abbrev CostructuredArrowDownwards.mk (comm : R.map a ≫ w.app X₁ ≫ B.map b
   CostructuredArrow.mk (Y := StructuredArrow.mk a)
     (StructuredArrow.homMk b (by simpa using comm))
 
-variable (comm : R.map a ≫ w.app X₁ ≫ B.map b = g)
 variable {w g}
 
 lemma StructuredArrowRightwards.mk_surjective
diff --git a/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean b/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
index 44a948a9222b1..b15c8b4f9117f 100644
--- a/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
+++ b/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
@@ -48,7 +48,7 @@ variable {C : Type u} [Category.{v} C]
 
 namespace PresheafOfGroups
 
-variable (G : Cᵒᵖ ⥤ Grp.{w}) {X : C} {I : Type w'} (U : I → C)
+variable (G : Cᵒᵖ ⥤ Grp.{w}) {I : Type w'} (U : I → C)
 
 /-- A zero cochain consists of a family of sections. -/
 def ZeroCochain := ∀ (i : I), G.obj (Opposite.op (U i))
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
index 6d675a7865092..2924a54b4d530 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@@ -34,8 +34,7 @@ open Fintype (card)
 
 namespace SimpleGraph
 
-variable {α β 𝕜 : Type*} [LinearOrderedField 𝕜] {G H : SimpleGraph α} {ε δ : 𝕜} {n : ℕ}
-  {s : Finset α}
+variable {α β 𝕜 : Type*} [LinearOrderedField 𝕜] {G H : SimpleGraph α} {ε δ : 𝕜}
 
 section LocallyLinear
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
index bff996c3fa38c..3de98cd5194b3 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
@@ -23,7 +23,7 @@ attribute [-instance] decidableEq_of_subsingleton
 
 open Finset Fintype
 
-variable {α : Type*} (G G' : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α}
+variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α}
 
 namespace SimpleGraph
 
@@ -146,7 +146,7 @@ private lemma triple_eq_triple_of_mem (hst : Disjoint s t) (hsu : Disjoint s u)
   · rintro rfl
     solve_by_elim
 
-variable [Fintype α] {P : Finpartition (univ : Finset α)}
+variable [Fintype α]
 
 /-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are disjoint sets of
 vertices such that each pair is `ε`-uniform and `2 * ε`-dense, then `G` contains at least
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
index 3135218de5e3d..c911166bc53ac 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@@ -38,7 +38,7 @@ This construction shows up unrelatedly twice in the theory of Roth numbers:
 open Finset Function Sum3
 
 variable {α β γ 𝕜 : Type*} [LinearOrderedField 𝕜] {t : Finset (α × β × γ)} {a a' : α} {b b' : β}
-  {c c' : γ} {x : α × β × γ} {ε : 𝕜}
+  {c c' : γ} {x : α × β × γ}
 
 namespace SimpleGraph
 namespace TripartiteFromTriangles
diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
index b43bd46488f69..5b1193b70b404 100644
--- a/Mathlib/Data/Real/Sqrt.lean
+++ b/Mathlib/Data/Real/Sqrt.lean
@@ -311,8 +311,6 @@ end Mathlib.Meta.Positivity
 
 namespace Real
 
-variable {x y : ℝ}
-
 @[simp]
 theorem sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x * y) = √x * √y := by
   simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index aafd0f1b3c5ef..670e4e5bf0347 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -80,7 +80,7 @@ theorem isPiSystem_pi [∀ i, MeasurableSpace (α i)] :
 
 section Finite
 
-variable [Finite ι] [Finite ι']
+variable [Finite ι]
 
 /-- Boxes of countably spanning sets are countably spanning. -/
 theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean
index 0cb212b5273b1..cad802e003d1f 100644
--- a/Mathlib/MeasureTheory/Group/Action.lean
+++ b/Mathlib/MeasureTheory/Group/Action.lean
@@ -28,7 +28,7 @@ namespace MeasureTheory
 
 universe u v w
 
-variable {G : Type u} {M : Type v} {α : Type w} {s : Set α}
+variable {G : Type u} {M : Type v} {α : Type w}
 
 namespace SMulInvariantMeasure
 
@@ -198,7 +198,7 @@ instance smulInvariantMeasure_map_smul [SMul M α] [SMul N α] [SMulCommClass N
 
 end SMulHomClass
 
-variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] (c : G) (μ : Measure α)
+variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure α)
 
 variable [MeasurableSpace G] [MeasurableSMul G α] in
 /-- Equivalent definitions of a measure invariant under a multiplicative action of a group.
diff --git a/Mathlib/MeasureTheory/Group/LIntegral.lean b/Mathlib/MeasureTheory/Group/LIntegral.lean
index e0344acdeed93..74c8453b516af 100644
--- a/Mathlib/MeasureTheory/Group/LIntegral.lean
+++ b/Mathlib/MeasureTheory/Group/LIntegral.lean
@@ -20,7 +20,7 @@ open Measure TopologicalSpace
 
 open scoped ENNReal
 
-variable {G : Type*} [MeasurableSpace G] {μ : Measure G} {g : G}
+variable {G : Type*} [MeasurableSpace G] {μ : Measure G}
 
 section MeasurableMul
 
diff --git a/Mathlib/MeasureTheory/Integral/Marginal.lean b/Mathlib/MeasureTheory/Integral/Marginal.lean
index 76fcaa682df92..4e19390aa37fb 100644
--- a/Mathlib/MeasureTheory/Integral/Marginal.lean
+++ b/Mathlib/MeasureTheory/Integral/Marginal.lean
@@ -66,7 +66,7 @@ section LMarginal
 
 variable {δ δ' : Type*} {π : δ → Type*} [∀ x, MeasurableSpace (π x)]
 variable {μ : ∀ i, Measure (π i)} [DecidableEq δ]
-variable {s t : Finset δ} {f g : (∀ i, π i) → ℝ≥0∞} {x y : ∀ i, π i} {i : δ}
+variable {s t : Finset δ} {f : (∀ i, π i) → ℝ≥0∞} {x : ∀ i, π i}
 
 /-- Integrate `f(x₁,…,xₙ)` over all variables `xᵢ` where `i ∈ s`. Return a function in the
   remaining variables (it will be constant in the `xᵢ` for `i ∈ s`).
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
index 4d2eb7fd31ab1..678a6983571d0 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -55,7 +55,7 @@ open Set Encodable Function Equiv Filter MeasureTheory
 
 universe uι
 
-variable {α β γ δ δ' : Type*} {ι : Sort uι} {s t u : Set α}
+variable {α β γ δ δ' : Type*} {ι : Sort uι} {s : Set α}
 
 namespace MeasurableSpace
 
@@ -225,7 +225,7 @@ variable {f g : α → β}
 
 section TypeclassMeasurableSpace
 
-variable [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+variable [MeasurableSpace α] [MeasurableSpace β]
 
 @[nontriviality, measurability]
 theorem Subsingleton.measurable [Subsingleton α] : Measurable f := fun _ _ =>
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean b/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
index e9f2db14bfc25..9dec6c3e39e9b 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
@@ -18,7 +18,7 @@ noncomputable section
 
 open Set MeasurableSpace
 
-variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
 
 /-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
   are countably spanning. -/
diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean
index ed27aa6936522..91b924e0a4f30 100644
--- a/Mathlib/MeasureTheory/Measure/Regular.lean
+++ b/Mathlib/MeasureTheory/Measure/Regular.lean
@@ -446,7 +446,7 @@ protected theorem FiniteSpanningSetsIn.outerRegular
 
 namespace InnerRegularWRT
 
-variable {p q : Set α → Prop} {U s : Set α} {ε r : ℝ≥0∞}
+variable {p : Set α → Prop}
 
 /-- If the restrictions of a measure to a monotone sequence of sets covering the space are
 inner regular for some property `p` and all measurable sets, then the measure itself is
@@ -637,7 +637,7 @@ end InnerRegularWRT
 
 namespace InnerRegular
 
-variable {U : Set α} {ε : ℝ≥0∞} [TopologicalSpace α]
+variable [TopologicalSpace α]
 
 /-- The measure of a measurable set is the supremum of the measures of compact sets it contains. -/
 theorem _root_.MeasurableSet.measure_eq_iSup_isCompact ⦃U : Set α⦄ (hU : MeasurableSet U)
diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
index af6dc235b4928..82a5c54c0a72c 100644
--- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
+++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@@ -636,8 +636,7 @@ end
 section mapAway
 
 variable [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜]
-variable {d e : ι} {f : A} (hf : f ∈ 𝒜 d) {g : A} (hg : g ∈ 𝒜 e)
-variable {x : A} (hx : x = f * g)
+variable {e : ι} {f : A} {g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g)
 
 variable (𝒜)
 
diff --git a/Mathlib/RingTheory/Localization/AtPrime.lean b/Mathlib/RingTheory/Localization/AtPrime.lean
index 65cccdc214ca9..76d9a9d2cb2e8 100644
--- a/Mathlib/RingTheory/Localization/AtPrime.lean
+++ b/Mathlib/RingTheory/Localization/AtPrime.lean
@@ -31,7 +31,7 @@ commutative ring, field of fractions
 -/
 
 
-variable {R : Type*} [CommSemiring R] (M : Submonoid R) (S : Type*) [CommSemiring S]
+variable {R : Type*} [CommSemiring R] (S : Type*) [CommSemiring S]
 variable [Algebra R S] {P : Type*} [CommSemiring P]
 
 section AtPrime
diff --git a/Mathlib/RingTheory/Localization/Integral.lean b/Mathlib/RingTheory/Localization/Integral.lean
index 07c55c2708e4b..ad327225f2383 100644
--- a/Mathlib/RingTheory/Localization/Integral.lean
+++ b/Mathlib/RingTheory/Localization/Integral.lean
@@ -25,7 +25,7 @@ commutative ring, field of fractions
 
 
 variable {R : Type*} [CommRing R] (M : Submonoid R) {S : Type*} [CommRing S]
-variable [Algebra R S] {P : Type*} [CommRing P]
+variable [Algebra R S]
 
 open Polynomial
 
diff --git a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean
index 62db6f2a12761..0637b7cd2c470 100644
--- a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean
+++ b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean
@@ -27,8 +27,7 @@ namespace IsLocalization
 
 section LocalizationLocalization
 
-variable {R : Type*} [CommSemiring R] (M : Submonoid R) {S : Type*} [CommSemiring S]
-variable [Algebra R S] {P : Type*} [CommSemiring P]
+variable {R : Type*} [CommSemiring R] (M : Submonoid R) {S : Type*} [CommSemiring S] [Algebra R S]
 variable (N : Submonoid S) (T : Type*) [CommSemiring T] [Algebra R T]
 
 
@@ -251,7 +250,7 @@ end IsLocalization
 
 namespace IsFractionRing
 
-variable {R : Type*} [CommRing R] (M : Submonoid R) {S : Type*} [CommRing S]
+variable {R : Type*} [CommRing R] (M : Submonoid R)
 
 open IsLocalization
 
diff --git a/Mathlib/RingTheory/TensorProduct/Free.lean b/Mathlib/RingTheory/TensorProduct/Free.lean
index 1f644e47cf568..a857cfdf874c6 100644
--- a/Mathlib/RingTheory/TensorProduct/Free.lean
+++ b/Mathlib/RingTheory/TensorProduct/Free.lean
@@ -30,7 +30,7 @@ namespace Algebra
 
 namespace TensorProduct
 
-variable {R S A : Type*}
+variable {R A : Type*}
 
 section Basis
 
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
index 680aa8f4249fe..4c69bfb655b75 100644
--- a/Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
+++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
@@ -15,8 +15,6 @@ import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
 * `Nat.instUniqueFactorizationMonoid`: the natural numbers have unique factorization
 -/
 
-variable {α : Type*}
-
 namespace Nat
 
 instance instWfDvdMonoid : WfDvdMonoid ℕ where
diff --git a/Mathlib/Testing/Plausible/Functions.lean b/Mathlib/Testing/Plausible/Functions.lean
index 9a83323198f47..a9bdf24d8ccb4 100644
--- a/Mathlib/Testing/Plausible/Functions.lean
+++ b/Mathlib/Testing/Plausible/Functions.lean
@@ -40,9 +40,9 @@ their defining property is invariant through shrinking. Injective
 functions are an example of how complicated it can get.
 -/
 
-universe u v w
+universe u v
 
-variable {α : Type u} {β : Type v} {γ : Sort w}
+variable {α : Type u} {β : Type v}
 
 namespace Plausible
 
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index 74529c1335d72..ba49c204bab72 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -21,12 +21,12 @@ noncomputable section
 
 open Filter Finset Function Topology
 
-variable {α β γ δ : Type*}
+variable {α β γ : Type*}
 
 section HasProd
 
 variable [CommMonoid α] [TopologicalSpace α]
-variable {f g : β → α} {a b : α} {s : Finset β}
+variable {f g : β → α} {a b : α}
 
 /-- Constant one function has product `1` -/
 @[to_additive "Constant zero function has sum `0`"]
@@ -355,7 +355,7 @@ end HasProd
 
 section tprod
 
-variable [CommMonoid α] [TopologicalSpace α] {f g : β → α} {a a₁ a₂ : α}
+variable [CommMonoid α] [TopologicalSpace α] {f g : β → α}
 
 @[to_additive]
 theorem tprod_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) :
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
index 8b1f1a092440e..4386fe90f6bd1 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
@@ -20,7 +20,7 @@ open Filter Finset Function
 
 open scoped Topology
 
-variable {α β γ δ : Type*}
+variable {α β γ : Type*}
 
 
 /-! ## Product, Sigma and Pi types -/
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
index 2bf685cd201e1..cc83507487809 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
@@ -111,7 +111,7 @@ notation3 "∏' "(...)", "r:67:(scoped f => tprod f) => r
 @[inherit_doc tsum]
 notation3 "∑' "(...)", "r:67:(scoped f => tsum f) => r
 
-variable {f g : β → α} {a b : α} {s : Finset β}
+variable {f : β → α} {a : α} {s : Finset β}
 
 @[to_additive]
 theorem HasProd.multipliable (h : HasProd f a) : Multipliable f :=
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 4c5353916aae3..937a415544928 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -20,7 +20,7 @@ open Filter Finset Function
 
 open scoped Topology
 
-variable {α β γ δ : Type*}
+variable {α β γ : Type*}
 
 section TopologicalGroup
 
@@ -197,7 +197,7 @@ theorem multipliable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} :
     Multipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b := by
   classical exact cauchy_map_iff_exists_tendsto.symm
 
-variable [UniformGroup α] {f g : β → α} {a a₁ a₂ : α}
+variable [UniformGroup α] {f g : β → α}
 
 @[to_additive]
 theorem cauchySeq_finset_iff_prod_vanishing :
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
index ea55550f54743..aa0cdf8f9a57d 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
@@ -19,12 +19,12 @@ This file provides lemmas about the interaction between infinite sums and multip
 
 open Filter Finset Function
 
-variable {ι κ R α : Type*}
+variable {ι κ α : Type*}
 
 section NonUnitalNonAssocSemiring
 
-variable [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f g : ι → α}
-  {a a₁ a₂ : α}
+variable [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α}
+  {a₁ : α}
 
 theorem HasSum.mul_left (a₂) (h : HasSum f a₁) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) := by
   simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)
@@ -63,8 +63,7 @@ end NonUnitalNonAssocSemiring
 
 section DivisionSemiring
 
-variable [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f g : ι → α}
-  {a a₁ a₂ : α}
+variable [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a a₁ a₂ : α}
 
 theorem HasSum.div_const (h : HasSum f a) (b : α) : HasSum (fun i ↦ f i / b) (a / b) := by
   simp only [div_eq_mul_inv, h.mul_right b⁻¹]
diff --git a/Mathlib/Topology/ContinuousMap/Ordered.lean b/Mathlib/Topology/ContinuousMap/Ordered.lean
index 5ef9876bb5f8c..7677b1c20ea56 100644
--- a/Mathlib/Topology/ContinuousMap/Ordered.lean
+++ b/Mathlib/Topology/ContinuousMap/Ordered.lean
@@ -13,8 +13,7 @@ import Mathlib.Topology.ContinuousMap.Defs
 -/
 
 
-variable {α : Type*} {β : Type*} {γ : Type*}
-variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
+variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
 
 namespace ContinuousMap
 
diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean
index 94b73607b7f71..029ada7f6a78a 100644
--- a/Mathlib/Topology/Instances/ENNReal.lean
+++ b/Mathlib/Topology/Instances/ENNReal.lean
@@ -25,7 +25,7 @@ variable {α : Type*} {β : Type*} {γ : Type*}
 
 namespace ENNReal
 
-variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0} {x y z : ℝ≥0∞} {ε ε₁ ε₂ : ℝ≥0∞} {s : Set ℝ≥0∞}
+variable {a b : ℝ≥0∞} {r : ℝ≥0} {x : ℝ≥0∞} {ε : ℝ≥0∞}
 
 section TopologicalSpace
 
diff --git a/Mathlib/Topology/MetricSpace/Dilation.lean b/Mathlib/Topology/MetricSpace/Dilation.lean
index 201c0e06799e3..6ab93147d696b 100644
--- a/Mathlib/Topology/MetricSpace/Dilation.lean
+++ b/Mathlib/Topology/MetricSpace/Dilation.lean
@@ -74,7 +74,7 @@ end Defs
 
 namespace Dilation
 
-variable {α : Type*} {β : Type*} {γ : Type*} {F : Type*} {G : Type*}
+variable {α : Type*} {β : Type*} {γ : Type*} {F : Type*}
 
 section Setup
 
@@ -229,8 +229,8 @@ end Setup
 section PseudoEmetricDilation
 
 variable [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
-variable [FunLike F α β] [DilationClass F α β] [FunLike G β γ] [DilationClass G β γ]
-variable (f : F) (g : G) {x y z : α} {s : Set α}
+variable [FunLike F α β] [DilationClass F α β]
+variable (f : F)
 
 /-- Every isometry is a dilation of ratio `1`. -/
 @[simps]
diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean
index 5e434b37434df..a987f5c09f284 100644
--- a/Mathlib/Topology/MetricSpace/Isometry.lean
+++ b/Mathlib/Topology/MetricSpace/Isometry.lean
@@ -62,7 +62,7 @@ namespace Isometry
 section PseudoEmetricIsometry
 
 variable [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
-variable {f : α → β} {x y z : α} {s : Set α}
+variable {f : α → β} {x : α}
 
 /-- An isometry preserves edistances. -/
 theorem edist_eq (hf : Isometry f) (x y : α) : edist (f x) (f y) = edist x y :=
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
index baa4f534f75cc..6183ec868a947 100644
--- a/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
+++ b/Mathlib/Topology/MetricSpace/Pseudo/Real.lean
@@ -15,7 +15,7 @@ open scoped NNReal Topology
 
 namespace Real
 
-variable {ι α : Type*} [PseudoMetricSpace α]
+variable {ι : Type*}
 
 lemma dist_left_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist x y ≤ dist x z := by
   simpa only [dist_comm x] using abs_sub_left_of_mem_uIcc h
@@ -35,7 +35,7 @@ lemma dist_le_of_mem_Icc {x y x' y' : ℝ} (hx : x ∈ Icc x' y') (hy : y ∈ Ic
 lemma dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 1) :
     dist x y ≤ 1 := by simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy
 
-variable {π : ι → Type*} [Fintype ι] [∀ i, PseudoMetricSpace (π i)] {x y x' y' : ι → ℝ}
+variable [Fintype ι] {x y x' y' : ι → ℝ}
 
 lemma dist_le_of_mem_pi_Icc (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ dist x' y' := by
   refine (dist_pi_le_iff dist_nonneg).2 fun b =>
diff --git a/Mathlib/Topology/Order/ExtrClosure.lean b/Mathlib/Topology/Order/ExtrClosure.lean
index d1b2049789057..31b06abf781bd 100644
--- a/Mathlib/Topology/Order/ExtrClosure.lean
+++ b/Mathlib/Topology/Order/ExtrClosure.lean
@@ -20,7 +20,7 @@ open Filter Set
 open Topology
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [Preorder Y]
-  [OrderClosedTopology Y] {f g : X → Y} {s : Set X} {a : X}
+  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X}
 
 protected theorem IsMaxOn.closure (h : IsMaxOn f s a) (hc : ContinuousOn f (closure s)) :
     IsMaxOn f (closure s) a := fun x hx =>
diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean
index bad7ee58b291e..7936b81bae9f3 100644
--- a/Mathlib/Topology/Order/MonotoneConvergence.lean
+++ b/Mathlib/Topology/Order/MonotoneConvergence.lean
@@ -107,7 +107,7 @@ end IsGLB
 
 section CiSup
 
-variable [ConditionallyCompleteLattice α] [SupConvergenceClass α] {f : ι → α} {a : α}
+variable [ConditionallyCompleteLattice α] [SupConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
     Tendsto f atTop (𝓝 (⨆ i, f i)) := by
@@ -121,7 +121,7 @@ end CiSup
 
 section CiInf
 
-variable [ConditionallyCompleteLattice α] [InfConvergenceClass α] {f : ι → α} {a : α}
+variable [ConditionallyCompleteLattice α] [InfConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
     Tendsto f atBot (𝓝 (⨅ i, f i)) := by convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1
@@ -133,7 +133,7 @@ end CiInf
 
 section iSup
 
-variable [CompleteLattice α] [SupConvergenceClass α] {f : ι → α} {a : α}
+variable [CompleteLattice α] [SupConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atTop_iSup (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) :=
   tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _)
@@ -145,7 +145,7 @@ end iSup
 
 section iInf
 
-variable [CompleteLattice α] [InfConvergenceClass α] {f : ι → α} {a : α}
+variable [CompleteLattice α] [InfConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atBot_iInf (h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i)) :=
   tendsto_atBot_ciInf h_mono (OrderBot.bddBelow _)
diff --git a/Mathlib/Topology/Order/T5.lean b/Mathlib/Topology/Order/T5.lean
index 39e0d08dc9b0a..597085db3f109 100644
--- a/Mathlib/Topology/Order/T5.lean
+++ b/Mathlib/Topology/Order/T5.lean
@@ -16,8 +16,7 @@ topological space.
 
 open Filter Set Function OrderDual Topology Interval
 
-variable {X : Type*} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a b c : X}
-  {s t : Set X}
+variable {X : Type*} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X}
 
 namespace Set
 
diff --git a/Mathlib/Topology/ShrinkingLemma.lean b/Mathlib/Topology/ShrinkingLemma.lean
index 8f03eeab6a068..65f6b72889730 100644
--- a/Mathlib/Topology/ShrinkingLemma.lean
+++ b/Mathlib/Topology/ShrinkingLemma.lean
@@ -206,7 +206,7 @@ section NormalSpace
 
 open ShrinkingLemma
 
-variable {u : ι → Set X} {s : Set X} {p : Set X → Prop} [NormalSpace X]
+variable {u : ι → Set X} {s : Set X} [NormalSpace X]
 
 /-- **Shrinking lemma**. A point-finite open cover of a closed subset of a normal space can be
 "shrunk" to a new open cover so that the closure of each new open set is contained in the
diff --git a/Mathlib/Topology/UniformSpace/OfCompactT2.lean b/Mathlib/Topology/UniformSpace/OfCompactT2.lean
index 5eaf71a852f4f..c9d49e9474570 100644
--- a/Mathlib/Topology/UniformSpace/OfCompactT2.lean
+++ b/Mathlib/Topology/UniformSpace/OfCompactT2.lean
@@ -26,7 +26,7 @@ uniform space, uniform continuity, compact space
 
 open Uniformity Topology Filter UniformSpace Set
 
-variable {α β γ : Type*} [UniformSpace α] [UniformSpace β]
+variable {γ : Type*}
 
 /-!
 ### Uniformity on compact spaces