chore: more unused variables (#18889)

#17715

Mathlib/Algebra/GroupWithZero/Action/Faithful.lean

@@ -16,7 +16,7 @@ assert_not_exists Ring
 
 open Function
 
-variable {M N A B α β : Type*}
+variable {α : Type*}
 
 /-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/
 instance CancelMonoidWithZero.faithfulSMul [CancelMonoidWithZero α] [Nontrivial α] :

Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean

@@ -23,12 +23,12 @@ assert_not_exists Ring
 open Function
 open scoped Pointwise
 
-variable {F α β γ : Type*}
+variable {α : Type*}
 
 namespace Set
 
 section MulZeroClass
-variable [MulZeroClass α] {s t : Set α}
+variable [MulZeroClass α] {s : Set α}
 
 /-! Note that `Set` is not a `MulZeroClass` because `0 * ∅ ≠ 0`. -/
 
@@ -44,7 +44,7 @@ lemma Nonempty.zero_mul (hs : s.Nonempty) : 0 * s = 0 :=
 end MulZeroClass
 
 section GroupWithZero
-variable [GroupWithZero α] {s t : Set α}
+variable [GroupWithZero α] {s : Set α}
 
 lemma div_zero_subset (s : Set α) : s / 0 ⊆ 0 := by simp [subset_def, mem_div]
 lemma zero_div_subset (s : Set α) : 0 / s ⊆ 0 := by simp [subset_def, mem_div]

Mathlib/Algebra/Lie/Derivation/Basic.lean

@@ -291,7 +291,7 @@ instance instBracket : Bracket (LieDerivation R L L) (LieDerivation R L L) where
       LinearMap.sub_apply, LinearMap.mul_apply, map_add, sub_lie, lie_sub, ← lie_skew b]
     abel)
 
-variable (D : LieDerivation R L L) {D1 D2 : LieDerivation R L L}
+variable {D1 D2 : LieDerivation R L L}
 
 @[simp]
 lemma commutator_coe_linear_map : ↑⁅D1, D2⁆ = ⁅(D1 : Module.End R L), (D2 : Module.End R L)⁆ :=

Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

@@ -34,7 +34,6 @@ variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
 variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
 variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
 variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
-variable (hp : p ≤ R⁰)
 variable (M' : Submodule R M)
 
 /-- Let `S` be the localization of `R` at `p` and `N` be the localization of `M` at `p`.

Mathlib/Algebra/Order/Algebra.lean

@@ -30,14 +30,7 @@ ordered algebra
 
 section OrderedAlgebra
 
-variable {R A : Type*} {a b : A} {r : R}
-
-
-
-variable [OrderedCommRing R] [OrderedRing A] [Algebra R A]
-
-
-variable [OrderedSMul R A]
+variable {R A : Type*} [OrderedCommRing R] [OrderedRing A] [Algebra R A] [OrderedSMul R A]
 
 theorem algebraMap_monotone : Monotone (algebraMap R A) := fun a b h => by
   rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -16,14 +16,13 @@ open Function
 open Fintype (card)
 open scoped BigOperators Pointwise NNRat
 
-variable {ι κ α β R : Type*}
+variable {ι α R : Type*}
 
 local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
 
 namespace Finset
 section OrderedAddCommMonoid
-variable [OrderedAddCommMonoid α] [Module ℚ≥0 α] [OrderedAddCommMonoid β] [Module ℚ≥0 β]
-  {s : Finset ι} {f g : ι → α}
+variable [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f g : ι → α}
 
 lemma expect_eq_zero_iff_of_nonneg (hs : s.Nonempty) (hf : ∀ i ∈ s, 0 ≤ f i) :
     𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
@@ -105,7 +104,7 @@ end PosSMulMono
 end OrderedAddCommMonoid
 
 section OrderedCancelAddCommMonoid
-variable [OrderedCancelAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f g : ι → α}
+variable [OrderedCancelAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α}
 section PosSMulStrictMono
 variable [PosSMulStrictMono ℚ≥0 α]
 
@@ -151,7 +150,7 @@ end Finset
 open Finset
 
 namespace Fintype
-variable [Fintype ι] [Fintype κ]
+variable [Fintype ι]
 
 section OrderedAddCommMonoid
 variable [OrderedAddCommMonoid α] [Module ℚ≥0 α] {f : ι → α}

Mathlib/Algebra/Order/Field/Pointwise.lean

@@ -16,8 +16,6 @@ This file contains lemmas about the effect of pointwise operations on sets with
 open Function Set
 open scoped Pointwise
 
-variable {α : Type*}
-
 namespace LinearOrderedField
 
 variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r)

Mathlib/Algebra/Order/Field/Power.lean

@@ -20,7 +20,7 @@ open Function Int
 
 section LinearOrderedSemifield
 
-variable [LinearOrderedSemifield α] {a b c d e : α} {m n : ℤ}
+variable [LinearOrderedSemifield α] {a b : α} {m n : ℤ}
 
 /-! ### Integer powers -/
 
@@ -91,7 +91,7 @@ end LinearOrderedSemifield
 
 section LinearOrderedField
 
-variable [LinearOrderedField α] {a b c d : α} {n : ℤ}
+variable [LinearOrderedField α] {a : α} {n : ℤ}
 
 protected theorem Even.zpow_nonneg (hn : Even n) (a : α) : 0 ≤ a ^ n := by
   obtain ⟨k, rfl⟩ := hn; rw [zpow_add' (by simp [em'])]; exact mul_self_nonneg _

Mathlib/Algebra/Order/Group/Indicator.lean

@@ -20,7 +20,7 @@ assert_not_exists MonoidWithZero
 
 open Set
 
-variable {ι : Sort*} {α β M : Type*}
+variable {ι : Sort*} {α M : Type*}
 
 namespace Function
 variable [One M]
@@ -59,7 +59,7 @@ end Function
 namespace Set
 
 section LE
-variable [LE M] [One M] {s t : Set α} {f g : α → M} {a : α} {y : M}
+variable [LE M] [One M] {s : Set α} {f g : α → M} {a : α} {y : M}
 
 @[to_additive]
 lemma mulIndicator_apply_le' (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) :
@@ -83,7 +83,7 @@ lemma le_mulIndicator (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a 
 end LE
 
 section Preorder
-variable [Preorder M] [One M] {s t : Set α} {f g : α → M} {a : α} {y : M}
+variable [Preorder M] [One M] {s t : Set α} {f g : α → M} {a : α}
 
 @[to_additive indicator_apply_nonneg]
 lemma one_le_mulIndicator_apply (h : a ∈ s → 1 ≤ f a) : 1 ≤ mulIndicator s f a :=
@@ -150,7 +150,7 @@ lemma indicator_nonpos_le_indicator (s : Set α) (f : α → M) :
 end LinearOrder
 
 section CompleteLattice
-variable [CompleteLattice M] [One M] {s t : Set α} {f g : α → M} {a : α} {y : M}
+variable [CompleteLattice M] [One M]
 
 @[to_additive]
 lemma mulIndicator_iUnion_apply (h1 : (⊥ : M) = 1) (s : ι → Set α) (f : α → M) (x : α) :

Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean

@@ -20,7 +20,7 @@ In this file we prove a few facts like “The infimum of `-s` is `-` the supremu
 open Function Set
 open scoped Pointwise
 
-variable {ι G M : Type*}
+variable {M : Type*}
 
 section ConditionallyCompleteLattice
 variable [ConditionallyCompleteLattice M]

Mathlib/Algebra/Order/Module/OrderedSMul.lean

@@ -53,11 +53,10 @@ class OrderedSMul (R M : Type*) [OrderedSemiring R] [OrderedAddCommMonoid M] [SM
   /-- If `c • a < c • b` for some positive `c`, then `a < b`. -/
   protected lt_of_smul_lt_smul_of_pos : ∀ {a b : M}, ∀ {c : R}, c • a < c • b → 0 < c → a < b
 
-variable {ι α β γ 𝕜 R M N : Type*}
+variable {ι 𝕜 R M N : Type*}
 
 section OrderedSMul
 variable [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M]
-  {s : Set M} {a b : M} {c : R}
 
 instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where
   elim _a ha _b₁ _b₂ hb := OrderedSMul.smul_lt_smul_of_pos hb ha
@@ -95,8 +94,7 @@ instance Int.orderedSMul [LinearOrderedAddCommGroup M] : OrderedSMul ℤ M :=
     · cases (Int.negSucc_not_pos _).1 hn
 
 section LinearOrderedSemiring
-variable [LinearOrderedSemiring R] [LinearOrderedAddCommMonoid M] [SMulWithZero R M]
-  [OrderedSMul R M] {a : R}
+variable [LinearOrderedSemiring R]
 
 -- TODO: `LinearOrderedField M → OrderedSMul ℚ M`
 instance LinearOrderedSemiring.toOrderedSMul : OrderedSMul R R :=

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -73,7 +73,7 @@ end Ring
 
 section Field
 
-variable {K : Type*} [Field K] [NeZero (2 : K)] {a b c x : K}
+variable {K : Type*} [Field K] [NeZero (2 : K)] {a b c : K}
 
 /-- Roots of a quadratic equation. -/
 theorem quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :

Mathlib/Algebra/Ring/Pointwise/Set.lean

@@ -22,7 +22,7 @@ assert_not_exists OrderedAddCommMonoid
 open Function
 open scoped Pointwise
 
-variable {F α β γ : Type*}
+variable {α : Type*}
 
 namespace Set
 

Mathlib/Analysis/Calculus/Deriv/Add.lean

@@ -29,12 +29,9 @@ open 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 : Filter 𝕜}
+variable {f g : 𝕜 → F}
+variable {f' g' : F}
+variable {x : 𝕜} {s : Set 𝕜} {L : Filter 𝕜}
 
 section Add
 

Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

@@ -30,10 +30,8 @@ namespace CategoryTheory
 
 open Localization
 
-variable {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃}
-  {D₁ : Type u₄} {D₂ : Type u₅} {D₃ : Type u₆}
-  [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} C₃]
-  [Category.{v₄} D₁] [Category.{v₅} D₂] [Category.{v₆} D₃]
+variable {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {D₁ : Type u₄} {D₂ : Type u₅}
+  [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} C₃] [Category.{v₄} D₁] [Category.{v₅} D₂]
   (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃)
 
 /-- If `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂`, a `LocalizerMorphism W₁ W₂`

Mathlib/CategoryTheory/Localization/SmallHom.lean

@@ -210,11 +210,9 @@ variable {C₁ : Type u₁} [Category.{v₁} C₁] {W₁ : MorphismProperty C₁
   (Φ : LocalizerMorphism W₁ W₂) (L₁ : C₁ ⥤ D₁) [L₁.IsLocalization W₁]
   (L₂ : C₂ ⥤ D₂) [L₂.IsLocalization W₂]
 
-variable {W}
-
 section
 
-variable {X Y Z : C₁}
+variable {X Y : C₁}
 
 variable [HasSmallLocalizedHom.{w} W₁ X Y]
   [HasSmallLocalizedHom.{w'} W₂ (Φ.functor.obj X) (Φ.functor.obj Y)]

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -404,7 +404,7 @@ theorem inv_tensor {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g]
     inv (f ⊗ g) = inv f ⊗ inv g := by
   simp [tensorHom_def ,whisker_exchange]
 
-variable {U V W X Y Z : C}
+variable {W X Y Z : C}
 
 theorem whiskerLeft_dite {P : Prop} [Decidable P]
     (X : C) {Y Z : C} (f : P → (Y ⟶ Z)) (f' : ¬P → (Y ⟶ Z)) :

Mathlib/Data/NNRat/Lemmas.lean

@@ -19,7 +19,7 @@ open Function
 open scoped NNRat
 
 namespace NNRat
-variable {α : Type*} {p q : ℚ≥0}
+variable {α : Type*} {q : ℚ≥0}
 
 /-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
 instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
@@ -60,7 +60,7 @@ end Rat
 
 namespace NNRat
 
-variable {p q : ℚ≥0}
+variable {q : ℚ≥0}
 
 /-- A recursor for nonnegative rationals in terms of numerators and denominators. -/
 protected def rec {α : ℚ≥0 → Sort*} (h : ∀ m n : ℕ, α (m / n)) (q : ℚ≥0) : α q := by

Mathlib/Data/Prod/TProd.lean

@@ -35,7 +35,7 @@ construction/theorem that is easier to define/prove on binary products than on f
 
 open List Function
 universe u v
-variable {ι : Type u} {α : ι → Type v} {i j : ι} {l : List ι} {f : ∀ i, α i}
+variable {ι : Type u} {α : ι → Type v} {i j : ι} {l : List ι}
 
 namespace List
 

Mathlib/Data/Real/Basic.lean

@@ -54,7 +54,7 @@ namespace Real
 
 open CauSeq CauSeq.Completion
 
-variable {x y : ℝ}
+variable {x : ℝ}
 
 theorem ext_cauchy_iff : ∀ {x y : Real}, x = y ↔ x.cauchy = y.cauchy
   | ⟨a⟩, ⟨b⟩ => by rw [ofCauchy.injEq]

Mathlib/Data/Sign.lean

@@ -392,7 +392,7 @@ end OrderedRing
 
 section LinearOrderedRing
 
-variable [LinearOrderedRing α] {a b : α}
+variable [LinearOrderedRing α]
 
 theorem sign_mul (x y : α) : sign (x * y) = sign x * sign y := by
   rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -40,8 +40,7 @@ universe u v w
 variable {R : Type*} {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
 variable {R₁ : Type*} {M₁ : Type*} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁]
 variable {V : Type*} {K : Type*} [Field K] [AddCommGroup V] [Module K V]
-variable {M' M'' : Type*}
-variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M'']
+variable {M' : Type*} [AddCommMonoid M'] [Module R M']
 variable {B : BilinForm R M} {B₁ : BilinForm R₁ M₁}
 
 namespace LinearMap
@@ -116,7 +115,6 @@ theorem isSymm_zero : (0 : BilinForm R M).IsSymm := fun _ _ => rfl
 theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm :=
   ⟨fun h => neg_neg B ▸ h.neg, IsSymm.neg⟩
 
-variable (R₂) in
 theorem isSymm_iff_flip : B.IsSymm ↔ flipHom B = B :=
   (forall₂_congr fun _ _ => by exact eq_comm).trans BilinForm.ext_iff.symm
 
@@ -201,7 +199,7 @@ theorem IsAdjointPair.sub (h : IsAdjointPair B₁ B₁' f₁ g₁) (h' : IsAdjoi
     IsAdjointPair B₁ B₁' (f₁ - f₁') (g₁ - g₁') := fun x y => by
   rw [LinearMap.sub_apply, LinearMap.sub_apply, sub_left, sub_right, h, h']
 
-variable {B₂' : BilinForm R M'} {f₂ f₂' : M →ₗ[R] M'} {g₂ g₂' : M' →ₗ[R] M}
+variable {B₂' : BilinForm R M'} {f₂ : M →ₗ[R] M'} {g₂ : M' →ₗ[R] M}
 
 theorem IsAdjointPair.smul (c : R) (h : IsAdjointPair B B₂' f₂ g₂) :
     IsAdjointPair B B₂' (c • f₂) (c • g₂) := fun x y => by

Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

@@ -36,7 +36,7 @@ Sesquilinear form, Sesquilinear map, matrix, basis
 -/
 
 
-variable {R R₁ S₁ R₂ S₂ M M₁ M₂ M₁' M₂' N₂ n m n' m' ι : Type*}
+variable {R R₁ S₁ R₂ S₂ M₁ M₂ M₁' M₂' N₂ n m n' m' ι : Type*}
 
 open Finset LinearMap Matrix
 
@@ -638,8 +638,6 @@ theorem _root_.Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinear
       (Matrix.toLinearMap₂ b b M).SeparatingLeft :=
   (separatingLeft_congr_iff b.equivFun.symm b.equivFun.symm).symm
 
-variable (B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁)
-
 -- Lemmas transferring nondegeneracy between a matrix and its associated bilinear form
 theorem _root_.Matrix.Nondegenerate.toLinearMap₂' {M : Matrix ι ι R₁} (h : M.Nondegenerate) :
     (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) := fun x hx =>

Mathlib/Order/Disjointed.lean

@@ -35,7 +35,7 @@ Related to the TODO in the module docstring of `Mathlib.Order.PartialSups`.
 -/
 
 
-variable {α β : Type*}
+variable {α : Type*}
 
 section GeneralizedBooleanAlgebra
 

Mathlib/RingTheory/Ideal/Prod.lean

@@ -17,7 +17,7 @@ product `I × J`, viewed as an ideal of `R × S`. In `ideal_prod_eq` we show tha
 
 universe u v
 
-variable {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I I' : Ideal R) (J J' : Ideal S)
+variable {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S)
 
 namespace Ideal
 

Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

@@ -15,7 +15,7 @@ theorem Ideal.isRadical_iff_quotient_reduced {R : Type*} [CommRing R] (I : Ideal
   conv_lhs => rw [← @Ideal.mk_ker R _ I]
   exact RingHom.ker_isRadical_iff_reduced_of_surjective (@Ideal.Quotient.mk_surjective R _ I)
 
-variable {R S : Type*} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S)
+variable {S : Type*} [CommRing S] (I : Ideal S)
 
 /-- Let `P` be a property on ideals. If `P` holds for square-zero ideals, and if
   `P I → P (J ⧸ I) → P J`, then `P` holds for all nilpotent ideals. -/

Mathlib/RingTheory/Localization/NumDen.lean

@@ -20,9 +20,6 @@ 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]
-
 namespace IsFractionRing
 
 open IsLocalization
@@ -157,6 +154,4 @@ lemma associated_num_den_inv (x : K) (hx : x ≠ 0) : Associated (num A x : A) (
 
 end NumDen
 
-variable (S)
-
 end IsFractionRing