chore: remove some unused variables (#17261)

Inspired by #17178 and found by a linter.

Mathlib/Algebra/Field/Basic.lean

@@ -167,7 +167,7 @@ end DivisionRing
 
 section Semifield
 
-variable [Semifield K] {a b c d : K}
+variable [Semifield K] {a b d : K}
 
 theorem div_add_div (a : K) (c : K) (hb : b ≠ 0) (hd : d ≠ 0) :
     a / b + c / d = (a * d + b * c) / (b * d) :=

Mathlib/Algebra/Group/Defs.lean

@@ -552,7 +552,7 @@ instance AddMonoid.toNatSMul {M : Type*} [AddMonoid M] : SMul ℕ M :=
 attribute [to_additive existing toNatSMul] Monoid.toNatPow
 
 section Monoid
-variable {M : Type*} [Monoid M] {a b c : M} {m n : ℕ}
+variable {M : Type*} [Monoid M] {a b c : M}
 
 @[to_additive (attr := simp) nsmul_eq_smul]
 theorem npow_eq_pow (n : ℕ) (x : M) : Monoid.npow n x = x ^ n :=
@@ -879,7 +879,7 @@ theorem exists_zpow_surjective (G : Type*) [Pow G ℤ] [IsCyclic G] :
 
 section DivInvMonoid
 
-variable [DivInvMonoid G] {a b : G}
+variable [DivInvMonoid G]
 
 @[to_additive (attr := simp) zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) :
     DivInvMonoid.zpow n x = x ^ n :=

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -130,7 +130,6 @@ instance (priority := 100) instMonoidHomClass
         _ = e (EquivLike.inv e (1 : N)) := by rw [← map_mul, one_mul]
         _ = 1 := EquivLike.right_inv e 1 }
 
-variable [EquivLike F α β]
 variable {F}
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -32,7 +32,7 @@ assert_not_exists DenselyOrdered
 
 open scoped Int
 
-variable {M G : Type*}
+variable {M : Type*}
 
 namespace SemiconjBy
 

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -291,7 +291,7 @@ end GroupWithZero
 
 section GroupWithZero
 
-variable [GroupWithZero G₀] {a b c : G₀}
+variable [GroupWithZero G₀] {a : G₀}
 
 @[simp]
 theorem zero_div (a : G₀) : 0 / a = 0 := by rw [div_eq_mul_inv, zero_mul]
@@ -421,7 +421,7 @@ end GroupWithZero
 
 section CommGroupWithZero
 
-variable [CommGroupWithZero G₀] {a b c d : G₀}
+variable [CommGroupWithZero G₀]
 
 theorem div_mul_eq_mul_div₀ (a b c : G₀) : a / c * b = a * b / c := by
   simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]

Mathlib/Algebra/GroupWithZero/Commute.lean

@@ -14,7 +14,7 @@ import Mathlib.Tactic.Nontriviality
 
 assert_not_exists DenselyOrdered
 
-variable {α M₀ G₀ M₀' G₀' F F' : Type*}
+variable {M₀ G₀ : Type*}
 variable [MonoidWithZero M₀]
 
 namespace Ring
@@ -83,7 +83,7 @@ theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c :=
 end Commute
 
 section GroupWithZero
-variable {G₀ : Type*} [GroupWithZero G₀] {a : G₀} {m n : ℕ}
+variable {G₀ : Type*} [GroupWithZero G₀]
 
 theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
   (Commute.refl a).inv_left₀.pow_pow m n

Mathlib/Algebra/GroupWithZero/InjSurj.lean

@@ -19,7 +19,7 @@ variable {M₀ G₀ M₀' G₀' : Type*}
 
 section MulZeroClass
 
-variable [MulZeroClass M₀] {a b : M₀}
+variable [MulZeroClass M₀]
 
 /-- Pull back a `MulZeroClass` instance along an injective function.
 See note [reducible non-instances]. -/

Mathlib/Algebra/GroupWithZero/Semiconj.lean

@@ -13,7 +13,7 @@ import Mathlib.Algebra.Group.Semiconj.Units
 
 assert_not_exists DenselyOrdered
 
-variable {α M₀ G₀ M₀' G₀' F F' : Type*}
+variable {G₀ : Type*}
 
 namespace SemiconjBy
 

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -94,7 +94,6 @@ def invMonoidWithZeroHom {G₀ : Type*} [CommGroupWithZero G₀] : G₀ →*₀
 namespace Units
 
 variable [GroupWithZero G₀]
-variable {a b : G₀}
 
 @[simp]
 theorem smul_mk0 {α : Type*} [SMul G₀ α] {g : G₀} (hg : g ≠ 0) (a : α) : mk0 g hg • a = g • a :=

Mathlib/Algebra/Module/BigOperators.lean

@@ -15,7 +15,7 @@ variable {ι κ α β R M : Type*}
 
 section AddCommMonoid
 
-variable [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x y : M)
+variable [Semiring R] [AddCommMonoid M] [Module R M]
 
 theorem List.sum_smul {l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
   map_list_sum ((smulAddHom R M).flip x) l

Mathlib/Algebra/Polynomial/Induction.lean

@@ -26,12 +26,11 @@ open Polynomial
 
 universe u v w x y z
 
-variable {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z} {a b : R}
-  {m n : ℕ}
+variable {R : Type u}
 
 section Semiring
 
-variable [Semiring R] {p q r : R[X]}
+variable [Semiring R]
 
 @[elab_as_elim]
 protected theorem induction_on {M : R[X] → Prop} (p : R[X]) (h_C : ∀ a, M (C a))

Mathlib/Algebra/Ring/Basic.lean

@@ -40,13 +40,6 @@ def mulRight [Distrib R] (r : R) : AddHom R R where
 
 end AddHom
 
-section AddHomClass
-
-variable {α β F : Type*} [NonAssocSemiring α] [NonAssocSemiring β]
-  [FunLike F α β] [AddHomClass F α β]
-
-end AddHomClass
-
 namespace AddMonoidHom
 
 /-- Left multiplication by an element of a (semi)ring is an `AddMonoidHom` -/
@@ -105,7 +98,7 @@ end HasDistribNeg
 
 section NonUnitalCommRing
 
-variable {α : Type*} [NonUnitalCommRing α] {a b c : α}
+variable {α : Type*} [NonUnitalCommRing α]
 
 attribute [local simp] add_assoc add_comm add_left_comm mul_comm
 

Mathlib/Algebra/Ring/Commute.lean

@@ -75,7 +75,7 @@ end
 
 section
 
-variable [MulOneClass R] [HasDistribNeg R] {a : R}
+variable [MulOneClass R] [HasDistribNeg R]
 
 -- Porting note (#10618): no longer needs to be `@[simp]` since `simp` can prove it.
 -- @[simp]
@@ -147,7 +147,7 @@ alias neg_one_pow_two := neg_one_sq
 end HasDistribNeg
 
 section Ring
-variable [Ring R] {a b : R} {n : ℕ}
+variable [Ring R] {a : R} {n : ℕ}
 
 @[simp] lemma neg_one_pow_mul_eq_zero_iff : (-1) ^ n * a = 0 ↔ a = 0 := by
   rcases neg_one_pow_eq_or R n with h | h <;> simp [h]

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -153,7 +153,6 @@ end coe
 section
 
 variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β]
-variable (f : α →ₙ+* β) {x y : α}
 
 @[ext]
 theorem ext ⦃f g : α →ₙ+* β⦄ : (∀ x, f x = g x) → f = g :=
@@ -225,7 +224,6 @@ theorem coe_comp (g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = g 
 @[simp]
 theorem comp_apply (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : g.comp f x = g (f x) :=
   rfl
-variable (g : β →ₙ+* γ) (f : α →ₙ+* β)
 
 @[simp]
 theorem coe_comp_addMonoidHom (g : β →ₙ+* γ) (f : α →ₙ+* β) :
@@ -441,7 +439,7 @@ end coe
 
 section
 
-variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β) {x y : α}
+variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β)
 
 protected theorem congr_fun {f g : α →+* β} (h : f = g) (x : α) : f x = g x :=
   DFunLike.congr_fun h x

Mathlib/Algebra/Ring/Semiconj.lean

@@ -19,9 +19,9 @@ For the definitions of semirings and rings see `Mathlib.Algebra.Ring.Defs`.
 -/
 
 
-universe u v w x
+universe u
 
-variable {α : Type u} {β : Type v} {γ : Type w} {R : Type x}
+variable {R : Type u}
 
 open Function
 
@@ -59,7 +59,7 @@ end
 
 section
 
-variable [MulOneClass R] [HasDistribNeg R] {a x y : R}
+variable [MulOneClass R] [HasDistribNeg R]
 
 -- Porting note: `simpNF` told me to remove `simp` attribute
 theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) :=

Mathlib/Algebra/Ring/Units.lean

@@ -49,7 +49,7 @@ end HasDistribNeg
 
 section Ring
 
-variable [Ring α] {a b : α}
+variable [Ring α]
 
 -- Needs to have higher simp priority than divp_add_divp. 1000 is the default priority.
 @[field_simps 1010]

Mathlib/Control/Basic.lean

@@ -214,8 +214,6 @@ class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulAppl
 
 open Functor
 
-variable {m}
-
 theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative m]
     [CommApplicative m] {α β γ} (a : m α) (b : m β) {f : α → β → γ} :
   f <$> a <*> b = flip f <$> b <*> a :=

Mathlib/Control/Lawful.lean

@@ -48,7 +48,7 @@ end StateT
 
 namespace ExceptT
 
-variable {α β ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α)
+variable {α ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α)
 
 -- Porting note: This is proven by proj reduction in Lean 3.
 @[simp]

Mathlib/Data/Subtype.lean

@@ -207,7 +207,7 @@ end Subtype
 namespace Subtype
 
 /-! Some facts about sets, which require that `α` is a type. -/
-variable {α β γ : Type*} {p : α → Prop}
+variable {α : Type*}
 
 @[simp]
 theorem coe_prop {S : Set α} (a : { a // a ∈ S }) : ↑a ∈ S :=

Mathlib/Lean/PrettyPrinter/Delaborator.lean

@@ -14,13 +14,6 @@ namespace Lean.PrettyPrinter.Delaborator
 
 open Lean.Meta Lean.SubExpr SubExpr
 
-namespace SubExpr
-
-variable {α : Type} [Inhabited α]
-variable {m : Type → Type} [Monad m]
-
-end SubExpr
-
 /-- Assuming the current expression in a lambda or pi,
 descend into the body using an unused name generated from the binder's name.
 Provides `d` with both `Syntax` for the bound name as an identifier

Mathlib/Logic/Basic.lean

@@ -435,8 +435,7 @@ end Equality
 section Quantifiers
 section Dependent
 
-variable {α : Sort*} {β : α → Sort*} {γ : ∀ a, β a → Sort*} {δ : ∀ a b, γ a b → Sort*}
-  {ε : ∀ a b c, δ a b c → Sort*}
+variable {α : Sort*} {β : α → Sort*} {γ : ∀ a, β a → Sort*}
 
 theorem pi_congr {β' : α → Sort _} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a :=
   (funext h : β = β') ▸ rfl
@@ -462,7 +461,7 @@ theorem Exists₃.imp {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c 
 
 end Dependent
 
-variable {α β : Sort*} {p q : α → Prop}
+variable {α β : Sort*} {p : α → Prop}
 
 theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
   ⟨fun f x y ↦ f y x, fun f x y ↦ f y x⟩
@@ -745,7 +744,7 @@ noncomputable def Exists.classicalRecOn {α : Sort*} {p : α → Prop} (h : ∃
 /-! ### Declarations about bounded quantifiers -/
 section BoundedQuantifiers
 
-variable {α : Sort*} {r p q : α → Prop} {P Q : ∀ x, p x → Prop} {b : Prop}
+variable {α : Sort*} {r p q : α → Prop} {P Q : ∀ x, p x → Prop}
 
 theorem bex_def : (∃ (x : _) (_ : p x), q x) ↔ ∃ x, p x ∧ q x :=
   ⟨fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩, fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩⟩

Mathlib/Logic/Equiv/Basic.lean

@@ -1580,8 +1580,6 @@ namespace Equiv
 
 section
 
-variable (P : α → Sort w) (e : α ≃ β)
-
 /-- Transport dependent functions through an equivalence of the base space.
 -/
 @[simps apply, simps (config := .lemmasOnly) symm_apply]

Mathlib/Logic/Function/Conjugate.lean

@@ -31,7 +31,7 @@ def Semiconj (f : α → β) (ga : α → α) (gb : β → β) : Prop :=
 
 namespace Semiconj
 
-variable {f fab : α → β} {fbc : β → γ} {ga ga' : α → α} {gb gb' : β → β} {gc gc' : γ → γ}
+variable {f fab : α → β} {fbc : β → γ} {ga ga' : α → α} {gb gb' : β → β} {gc : γ → γ}
 
 /-- Definition of `Function.Semiconj` in terms of functional equality. -/
 lemma _root_.Function.semiconj_iff_comp_eq : Semiconj f ga gb ↔ f ∘ ga = gb ∘ f := funext_iff.symm

Mathlib/Logic/Relator.lean

@@ -96,8 +96,8 @@ lemma rel_not : (Iff ⇒ Iff) Not Not :=
 lemma bi_total_eq {α : Type u₁} : Relator.BiTotal (@Eq α) :=
   { left := fun a => ⟨a, rfl⟩, right := fun a => ⟨a, rfl⟩ }
 
-variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
-variable {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}
+variable {α : Type*} {β : Type*} {γ : Type*}
+variable {r : α → β → Prop}
 
 lemma LeftUnique.flip (h : LeftUnique r) : RightUnique (flip r) :=
   fun _ _ _ h₁ h₂ => h h₁ h₂

Mathlib/Logic/Unique.lean

@@ -247,7 +247,6 @@ instance {α} [IsEmpty α] : Unique (Option α) :=
 end Option
 
 section Subtype
-variable {α : Sort u}
 
 instance Unique.subtypeEq (y : α) : Unique { x // x = y } where
   default := ⟨y, rfl⟩

Mathlib/Order/Basic.lean

@@ -186,7 +186,7 @@ end
 
 namespace Eq
 
-variable [Preorder α] {x y z : α}
+variable [Preorder α] {x y : α}
 
 /-- If `x = y` then `y ≤ x`. Note: this lemma uses `y ≤ x` instead of `x ≥ y`, because `le` is used
 almost exclusively in mathlib. -/

Mathlib/Order/Defs.lean

@@ -552,7 +552,6 @@ lemma max_lt (h₁ : a < c) (h₂ : b < c) : max a b < c := by
   cases le_total a b <;> simp [max_eq_left, max_eq_right, *]
 
 section Ord
-variable {o : Ordering}
 
 lemma compare_lt_iff_lt : compare a b = .lt ↔ a < b := by
   rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]

Mathlib/Order/Interval/Finset/Basic.lean

@@ -683,7 +683,7 @@ variable [LinearOrder α]
 
 section LocallyFiniteOrder
 
-variable [LocallyFiniteOrder α] {a b : α}
+variable [LocallyFiniteOrder α]
 
 theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
     Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
@@ -790,7 +790,7 @@ end LinearOrder
 
 section Lattice
 
-variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ x : α}
 
 theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding :=
   Icc_toDual _ _
@@ -862,7 +862,7 @@ end Lattice
 
 section DistribLattice
 
-variable [DistribLattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [DistribLattice α] [LocallyFiniteOrder α] {a b c : α}
 
 theorem eq_of_mem_uIcc_of_mem_uIcc : a ∈ [[b, c]] → b ∈ [[a, c]] → a = b := by
   simp_rw [mem_uIcc]
@@ -883,7 +883,7 @@ end DistribLattice
 
 section LinearOrder
 
-variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c : α}
 
 theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
   rfl

Mathlib/Order/Max.lean

@@ -356,7 +356,7 @@ end PartialOrder
 
 section Prod
 
-variable [Preorder α] [Preorder β] {a a₁ a₂ : α} {b b₁ b₂ : β} {x y : α × β}
+variable [Preorder α] [Preorder β] {a : α} {b : β} {x : α × β}
 
 theorem IsBot.prod_mk (ha : IsBot a) (hb : IsBot b) : IsBot (a, b) := fun _ => ⟨ha _, hb _⟩