feat: the unusedVariableCommand linter

Mathlib.lean

@@ -4979,6 +4979,7 @@ import Mathlib.Tactic.Linter.RefineLinter
 import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Linter.TextBased
 import Mathlib.Tactic.Linter.UnusedTactic
+import Mathlib.Tactic.Linter.UnusedVariableCommand
 import Mathlib.Tactic.Linter.UpstreamableDecl
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init

Mathlib/Algebra/Group/Idempotent.lean

@@ -27,7 +27,7 @@ projection, idempotent
 
 assert_not_exists GroupWithZero
 
-variable {M N S : Type*}
+variable {M S : Type*}
 
 /-- An element `a` is said to be idempotent if `a * a = a`. -/
 def IsIdempotentElem [Mul M] (a : M) : Prop := a * a = a

Mathlib/Algebra/GroupWithZero/Idempotent.lean

@@ -12,10 +12,10 @@ import Mathlib.Algebra.GroupWithZero.Defs
 
 assert_not_exists Ring
 
-variable {M N S M₀ M₁ R G G₀ : Type*}
-variable [MulOneClass M₁] [CancelMonoidWithZero G₀]
+variable {M₀ G₀ : Type*}
 
 namespace IsIdempotentElem
+
 section MulZeroClass
 variable [MulZeroClass M₀]
 
@@ -28,7 +28,8 @@ instance : Zero { p : M₀ // IsIdempotentElem p } where zero := ⟨0, zero⟩
 end MulZeroClass
 
 section CancelMonoidWithZero
-variable [CancelMonoidWithZero M₀]
+
+variable [CancelMonoidWithZero G₀]
 
 @[simp]
 lemma iff_eq_zero_or_one {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1 where

Mathlib/Data/Finite/Defs.lean

@@ -228,8 +228,6 @@ namespace Set
 
 /-! ### Infinite sets -/
 
-variable {s t : Set α}
-
 theorem infinite_coe_iff {s : Set α} : Infinite s ↔ s.Infinite :=
   not_finite_iff_infinite.symm.trans finite_coe_iff.not
 

Mathlib/Data/Int/Cast/Field.lean

@@ -16,24 +16,24 @@ This file concerns the canonical homomorphism `ℤ → F`, where `F` is a field.
  * `Int.cast_div`: if `n` divides `m`, then `↑(m / n) = ↑m / ↑n`
 -/
 
-
 namespace Int
 
 open Nat
 
-variable {α : Type*}
+variable {R : Type*} [DivisionRing R]
 
 /-- Auxiliary lemma for norm_cast to move the cast `-↑n` upwards to `↑-↑n`.
 
 (The restriction to `DivisionRing` is necessary, otherwise this would also apply in the case where
 `R = ℤ` and cause nontermination.)
 -/
 @[norm_cast]
-theorem cast_neg_natCast {R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
+theorem cast_neg_natCast (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
+
 
 @[simp]
-theorem cast_div [DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : α) ≠ 0) :
-    ((m / n : ℤ) : α) = m / n := by
+theorem cast_div {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : R) ≠ 0) :
+    ((m / n : ℤ) : R) = m / n := by
   rcases n_dvd with ⟨k, rfl⟩
   have : n ≠ 0 := by rintro rfl; simp at hn
   rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

@@ -50,7 +50,7 @@ variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]
-  {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} (t₀ : ℝ) {x₀ : M}
+  {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} (t₀ : ℝ) {x₀ : M}
 
 /-- Existence of local integral curves for a $C^1$ vector field at interior points of a `C^1`
 manifold. -/

Mathlib/Init.lean

@@ -7,8 +7,9 @@ import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.Multigoal
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.RefineLinter
-import Mathlib.Tactic.Linter.UnusedTactic
 import Mathlib.Tactic.Linter.Style
+import Mathlib.Tactic.Linter.UnusedTactic
+import Mathlib.Tactic.Linter.UnusedVariableCommand
 
 /-!
 This is the root file in Mathlib: it is imported by virtually *all* Mathlib files.

Mathlib/MeasureTheory/Function/LpSpace/DomAct/Continuous.lean

@@ -38,7 +38,7 @@ namespace MeasureTheory
 
 variable {X M E : Type*}
   [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X]
-  [Monoid M] [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M]
+  [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M]
   [SMul M X] [ContinuousSMul M X]
   [NormedAddCommGroup E]
   {μ : Measure X} [IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop]

Mathlib/NumberTheory/LSeries/PrimesInAP.lean

@@ -75,7 +75,7 @@ as an iterated product or sum over primes and natural numbers.
 
 section auxiliary
 
-variable {α β γ : Type*} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α]
+variable {α : Type*} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α]
   [T0Space α]
 
 open Nat.Primes in

Mathlib/Order/BoundedOrder/Basic.lean

@@ -92,7 +92,7 @@ attribute [aesop (rule_sets := [finiteness]) unsafe 20%] ne_top_of_lt
 
 end Preorder
 
-variable [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a b : α}
+variable [PartialOrder α] [OrderTop α] {f : α → β} {a b : α}
 
 @[simp]
 theorem isMax_iff_eq_top : IsMax a ↔ a = ⊤ :=
@@ -253,7 +253,7 @@ alias LT.lt.bot_lt := bot_lt_of_lt
 
 end Preorder
 
-variable [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a b : α}
+variable [PartialOrder α] [OrderBot α] {f : α → β} {a b : α}
 
 @[simp]
 theorem isMin_iff_eq_bot : IsMin a ↔ a = ⊥ :=

Mathlib/Order/BoundedOrder/Lattice.lean

@@ -24,9 +24,9 @@ instances for `Prop` and `fun`.
 
 open Function OrderDual
 
-universe u v
+universe u
 
-variable {α : Type u} {β : Type v}
+variable {α : Type u}
 
 /-! ### Top, bottom element -/
 

Mathlib/Order/BoundedOrder/Monotone.lean

@@ -23,7 +23,7 @@ variable {α : Type u} {β : Type v}
 
 section OrderTop
 
-variable [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a b : α}
+variable [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α}
 
 theorem StrictMono.apply_eq_top_iff (hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤ :=
   ⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne h, congr_arg _⟩
@@ -43,7 +43,7 @@ theorem StrictMono.maximal_preimage_top [LinearOrder α] [Preorder β] [OrderTop
 
 section OrderBot
 
-variable [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a b : α}
+variable [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α}
 
 theorem StrictMono.apply_eq_bot_iff (hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥ :=
   hf.dual.apply_eq_top_iff

Mathlib/Order/Monotone/Monovary.lean

@@ -24,7 +24,6 @@ This condition comes up in the rearrangement inequality. See `Algebra.Order.Rear
 * `AntivaryOn f g s`: `f` antivaries with `g` on `s`.
 -/
 
-
 open Function Set
 
 variable {ι ι' α β γ : Type*}

Mathlib/Tactic.lean

@@ -153,6 +153,7 @@ import Mathlib.Tactic.Linter.RefineLinter
 import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Linter.TextBased
 import Mathlib.Tactic.Linter.UnusedTactic
+import Mathlib.Tactic.Linter.UnusedVariableCommand
 import Mathlib.Tactic.Linter.UpstreamableDecl
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init