chore: remove unused variables (#18226)

#17715
leanprover-community · Oct 25, 2024 · a4411e6 · a4411e6
1 parent 27e4d0a
commit a4411e6
Show file tree

Hide file tree

Showing 16 changed files with 23 additions and 25 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 }