chore: remove some unused variables

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -400,7 +400,7 @@ end CommSemiring
 
 section CommRing
 
-variable {F R A B : Type*} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
+variable {F R A : Type*} [CommRing R] [Ring A] [Algebra R A]
 variable [FunLike F A R] [AlgHomClass F R A R]
 
 local notation "σ" => spectrum R

Mathlib/Algebra/Group/Basic.lean

@@ -172,7 +172,7 @@ end CommSemigroup
 attribute [local simp] mul_assoc sub_eq_add_neg
 
 section Monoid
-variable [Monoid M] {a b c : M} {m n : ℕ}
+variable [Monoid M] {a b : M} {m n : ℕ}
 
 @[to_additive boole_nsmul]
 lemma pow_boole (P : Prop) [Decidable P] (a : M) :
@@ -316,7 +316,7 @@ end InvolutiveInv
 
 section DivInvMonoid
 
-variable [DivInvMonoid G] {a b c : G}
+variable [DivInvMonoid G]
 
 @[to_additive, field_simps] -- The attributes are out of order on purpose
 theorem inv_eq_one_div (x : G) : x⁻¹ = 1 / x := by rw [div_eq_mul_inv, one_mul]

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -181,7 +181,7 @@ end Monoid
 
 section DivisionMonoid
 
-variable [DivisionMonoid G] {a b c d : G}
+variable [DivisionMonoid G] {a b : G}
 
 @[to_additive]
 protected theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -958,8 +958,6 @@ instance [MulOneClass M] [MulOneClass N] : Inhabited (M →* N) := ⟨1⟩
 
 namespace MonoidHom
 
-variable [Group G] [CommGroup H]
-
 @[to_additive (attr := simp)]
 theorem one_comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) :
     (1 : N →* P).comp f = 1 := rfl

Mathlib/Algebra/Group/Semiconj/Defs.lean

@@ -115,7 +115,7 @@ end Monoid
 
 section Group
 
-variable [Group G] {a x y : G}
+variable [Group G]
 
 /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
 @[to_additive "`a` semiconjugates `x` to `a + x + -a`."]

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -159,17 +159,17 @@ class MulDivCancelClass (M₀ : Type*) [MonoidWithZero M₀] [Div M₀] : Prop w
   protected mul_div_cancel (a b : M₀) : b ≠ 0 → a * b / b = a
 
 section MulDivCancelClass
-variable [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {a b : M₀}
+variable [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀]
 
-@[simp] lemma mul_div_cancel_right₀ (a : M₀) (hb : b ≠ 0) : a * b / b = a :=
+@[simp] lemma mul_div_cancel_right₀ (a : M₀) {b : M₀} (hb : b ≠ 0) : a * b / b = a :=
   MulDivCancelClass.mul_div_cancel _ _ hb
 
 end MulDivCancelClass
 
 section MulDivCancelClass
-variable [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {a b : M₀}
+variable [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀]
 
-@[simp] lemma mul_div_cancel_left₀ (b : M₀) (ha : a ≠ 0) : a * b / a = b := by
+@[simp] lemma mul_div_cancel_left₀ {a : M₀} (b : M₀) (ha : a ≠ 0) : a * b / a = b := by
   rw [mul_comm, mul_div_cancel_right₀ _ ha]
 
 end MulDivCancelClass
@@ -216,7 +216,7 @@ end
 
 section GroupWithZero
 
-variable [GroupWithZero G₀] {a b c g h x : G₀}
+variable [GroupWithZero G₀] {a b : G₀}
 
 @[simp]
 theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=

Mathlib/Algebra/Polynomial/Smeval.lean

@@ -180,7 +180,7 @@ the defining structures independently.  For non-associative power-associative al
 octonions), we replace the `[Semiring S]` with `[NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S]`.
 -/
 
-variable (R : Type*) [Semiring R] {p : R[X]} (r : R) (p q : R[X]) {S : Type*}
+variable (R : Type*) [Semiring R] (r : R) (p q : R[X]) {S : Type*}
   [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S)
 
 theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x := by

Mathlib/Algebra/Ring/Defs.lean

@@ -250,7 +250,7 @@ instance (priority := 100) CommSemiring.toCommMonoidWithZero [CommSemiring α] :
 
 section CommSemiring
 
-variable [CommSemiring α] {a b c : α}
+variable [CommSemiring α]
 
 theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
   simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

Mathlib/Control/Traversable/Lemmas.lean

@@ -56,7 +56,7 @@ def PureTransformation :
 theorem pureTransformation_apply {α} (x : id α) : PureTransformation F x = pure x :=
   rfl
 
-variable {F G} (x : t β)
+variable {F G}
 
 -- Porting note: need to specify `m/F/G := Id` because `id` no longer has a `Monad` instance
 theorem map_eq_traverse_id : map (f := t) f = traverse (m := Id) (pure ∘ f) :=

Mathlib/Data/Int/Defs.lean

@@ -30,7 +30,6 @@ namespace Int
 variable {a b c d m n : ℤ}
 
 section Order
-variable {a b c : ℤ}
 
 protected lemma le_rfl : a ≤ a := a.le_refl
 protected lemma lt_or_lt_of_ne : a ≠ b → a < b ∨ b < a := Int.lt_or_gt_of_ne

Mathlib/Data/List/Count.lean

@@ -19,7 +19,7 @@ assert_not_exists Ring
 
 open Nat
 
-variable {α : Type*} {l : List α}
+variable {α : Type*}
 
 namespace List
 

Mathlib/Data/Set/Basic.lean

@@ -1958,7 +1958,7 @@ open Set
 
 namespace Function
 
-variable {ι : Sort*} {α : Type*} {β : Type*} {f : α → β}
+variable {α : Type*} {β : Type*}
 
 theorem Injective.nonempty_apply_iff {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅)
     {s : Set α} : (f s).Nonempty ↔ s.Nonempty := by
@@ -2141,7 +2141,7 @@ end Monotone
 
 /-! ### Disjoint sets -/
 
-variable {α β : Type*} {s t u : Set α} {f : α → β}
+variable {α : Type*} {s t u : Set α}
 
 namespace Disjoint
 

Mathlib/Data/Sum/Basic.lean

@@ -35,7 +35,7 @@ theorem sum_rec_congr (P : α ⊕ β → Sort*) (f : ∀ i, P (inl i)) (g : ∀
 
 section get
 
-variable {x y : α ⊕ β}
+variable {x : α ⊕ β}
 
 theorem eq_left_iff_getLeft_eq {a : α} : x = inl a ↔ ∃ h, x.getLeft h = a := by
   cases x <;> simp

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -68,7 +68,7 @@ structure LocalInvariantProp (P : (H → H') → Set H → H → Prop) : Prop wh
   left_invariance' : ∀ {s x f} {e' : PartialHomeomorph H' H'},
     e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (e' ∘ f) s x
 
-variable {G G'} {P : (H → H') → Set H → H → Prop} {s t u : Set H} {x : H}
+variable {G G'} {P : (H → H') → Set H → H → Prop}
 variable (hG : G.LocalInvariantProp G' P)
 include hG
 

Mathlib/Logic/Lemmas.lean

@@ -24,7 +24,7 @@ theorem iff_right_comm {a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
 
 protected alias ⟨HEq.eq, Eq.heq⟩ := heq_iff_eq
 
-variable {α : Sort*} {p q r : Prop} [Decidable p] [Decidable q] {a b c : α}
+variable {α : Sort*} {p q : Prop} [Decidable p] [Decidable q] {a b c : α}
 
 theorem dite_dite_distrib_left {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :
     (dite p a fun hp ↦ dite q (b hp) (c hp)) =

Mathlib/Order/BoundedOrder.lean

@@ -353,7 +353,7 @@ theorem OrderBot.ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : Par
 
 section SemilatticeSupTop
 
-variable [SemilatticeSup α] [OrderTop α] {a : α}
+variable [SemilatticeSup α] [OrderTop α]
 
 -- Porting note: Not simp because simp can prove it
 theorem top_sup_eq (a : α) : ⊤ ⊔ a = ⊤ :=
@@ -400,7 +400,7 @@ end SemilatticeInfTop
 
 section SemilatticeInfBot
 
-variable [SemilatticeInf α] [OrderBot α] {a : α}
+variable [SemilatticeInf α] [OrderBot α]
 
 -- Porting note: Not simp because simp can prove it
 lemma bot_inf_eq (a : α) : ⊥ ⊓ a = ⊥ := inf_of_le_left bot_le

Mathlib/Order/Disjoint.lean

@@ -108,7 +108,7 @@ end PartialBoundedOrder
 
 section SemilatticeInfBot
 
-variable [SemilatticeInf α] [OrderBot α] {a b c d : α}
+variable [SemilatticeInf α] [OrderBot α] {a b c : α}
 
 theorem disjoint_iff_inf_le : Disjoint a b ↔ a ⊓ b ≤ ⊥ :=
   ⟨fun hd ↦ hd inf_le_left inf_le_right, fun h _ ha hb ↦ (le_inf ha hb).trans h⟩
@@ -267,7 +267,7 @@ end PartialBoundedOrder
 
 section SemilatticeSupTop
 
-variable [SemilatticeSup α] [OrderTop α] {a b c d : α}
+variable [SemilatticeSup α] [OrderTop α] {a b c : α}
 
 theorem codisjoint_iff_le_sup : Codisjoint a b ↔ ⊤ ≤ a ⊔ b :=
   @disjoint_iff_inf_le αᵒᵈ _ _ _ _
@@ -401,7 +401,7 @@ namespace IsCompl
 
 section BoundedPartialOrder
 
-variable [PartialOrder α] [BoundedOrder α] {x y z : α}
+variable [PartialOrder α] [BoundedOrder α] {x y : α}
 
 @[symm]
 protected theorem symm (h : IsCompl x y) : IsCompl y x :=
@@ -419,7 +419,7 @@ end BoundedPartialOrder
 
 section BoundedLattice
 
-variable [Lattice α] [BoundedOrder α] {x y z : α}
+variable [Lattice α] [BoundedOrder α] {x y : α}
 
 theorem of_le (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y :=
   ⟨disjoint_iff_inf_le.mpr h₁, codisjoint_iff_le_sup.mpr h₂⟩

Mathlib/Order/Lattice.lean

@@ -528,7 +528,7 @@ def Lattice.mk' {α : Type*} [Sup α] [Inf α] (sup_comm : ∀ a b : α, a ⊔ b
 
 section Lattice
 
-variable [Lattice α] {a b c d : α}
+variable [Lattice α] {a b c : α}
 
 theorem inf_le_sup : a ⊓ b ≤ a ⊔ b :=
   inf_le_left.trans le_sup_left

Mathlib/Order/Monotone/Basic.lean

@@ -1025,7 +1025,7 @@ theorem Subtype.strictMono_coe [Preorder α] (t : Set α) :
 
 section Preorder
 
-variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} {a b : α}
+variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ}
 
 theorem monotone_fst : Monotone (@Prod.fst α β) := fun _ _ ↦ And.left
 

Mathlib/RingTheory/Nilpotent/Lemmas.lean

@@ -31,16 +31,6 @@ theorem isRadical_iff_span_singleton [CommSemiring R] :
   simp_rw [IsRadical, ← Ideal.mem_span_singleton]
   exact forall_swap.trans (forall_congr' fun r => exists_imp.symm)
 
-namespace Commute
-
-section Semiring
-
-variable [Semiring R] (h_comm : Commute x y)
-
-end Semiring
-
-end Commute
-
 section CommSemiring
 
 variable [CommSemiring R] {x y : R}