chore: remove more unused variables (#17749)

Mathlib/Algebra/Group/Action/Pi.lean

@@ -21,7 +21,7 @@ This file defines instances for `MulAction` and related structures on `Pi` types
 
 assert_not_exists MonoidWithZero
 
-variable {ι M N : Type*} {α β γ : ι → Type*} (x y : ∀ i, α i) (i : ι)
+variable {ι M N : Type*} {α β γ : ι → Type*} (i : ι)
 
 namespace Pi
 

Mathlib/Algebra/Group/Units/Defs.lean

@@ -170,7 +170,7 @@ the `AddMonoid`."]
 instance [Repr α] : Repr αˣ :=
   ⟨reprPrec ∘ val⟩
 
-variable (a b c : αˣ) {u : αˣ}
+variable (a b : αˣ) {u : αˣ}
 
 @[to_additive (attr := simp, norm_cast)]
 theorem val_mul : (↑(a * b) : α) = a * b :=
@@ -477,7 +477,7 @@ theorem mul_iff [CommMonoid M] {x y : M} : IsUnit (x * y) ↔ IsUnit x ∧ IsUni
 
 section Monoid
 
-variable [Monoid M] {a b c : M}
+variable [Monoid M] {a : M}
 
 /-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
 `α` is a `DivisionMonoid`, use `IsUnit.unit'` instead. -/
@@ -577,7 +577,7 @@ protected lemma mul_div_mul_right (h : IsUnit c) (a b : α) : a * c / (b * c) =
 end DivisionMonoid
 
 section DivisionCommMonoid
-variable [DivisionCommMonoid α] {a b c d : α}
+variable [DivisionCommMonoid α] {a c : α}
 
 @[to_additive]
 protected lemma div_mul_cancel_left (h : IsUnit a) (b : α) : a / (a * b) = b⁻¹ := by

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -31,7 +31,7 @@ assert_not_exists DenselyOrdered
 
 open Function
 
-variable {M : Type*} {N : Type*} {G : Type*} {H : Type*}
+variable {M : Type*} {G : Type*} {H : Type*}
 
 /-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/
 theorem hom_coe_pow {F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id)

Mathlib/Algebra/Order/Group/Prod.lean

@@ -11,8 +11,6 @@ import Mathlib.Algebra.Order.Monoid.Prod
 -/
 
 
-variable {α : Type*}
-
 namespace Prod
 
 variable {G H : Type*}

Mathlib/Algebra/Order/Monovary.lean

@@ -26,7 +26,7 @@ variable {ι α β : Type*}
 /-! ### Algebraic operations on monovarying functions -/
 
 section OrderedCommGroup
-variable [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f f₁ f₂ : ι → α} {g g₁ g₂ : ι → β}
+variable [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f f₁ f₂ : ι → α} {g : ι → β}
 
 @[to_additive (attr := simp)]
 lemma monovaryOn_inv_left : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s := by
@@ -118,7 +118,7 @@ lemma Antivary.div_left (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) : Anti
 end OrderedCommGroup
 
 section LinearOrderedCommGroup
-variable [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f f₁ f₂ : ι → α}
+variable [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α}
   {g g₁ g₂ : ι → β}
 
 @[to_additive] lemma MonovaryOn.mul_right (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
@@ -168,7 +168,7 @@ variable [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f f₁
 end LinearOrderedCommGroup
 
 section OrderedSemiring
-variable [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f f₁ f₂ : ι → α} {g g₁ g₂ : ι → β}
+variable [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f f₁ f₂ : ι → α} {g : ι → β}
 
 lemma MonovaryOn.mul_left₀ (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 ≤ f₂ i)
     (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : MonovaryOn (f₁ * f₂) g s :=
@@ -201,7 +201,7 @@ lemma Antivary.pow_left₀ (hf : 0 ≤ f) (hfg : Antivary f g) (n : ℕ) : Antiv
 end OrderedSemiring
 
 section LinearOrderedSemiring
-variable [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f f₁ f₂ : ι → α}
+variable [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f : ι → α}
   {g g₁ g₂ : ι → β}
 
 lemma MonovaryOn.mul_right₀ (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 ≤ g₂ i)
@@ -325,7 +325,7 @@ end LinearOrderedSemifield
 
 section LinearOrderedAddCommGroup
 variable [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β]
-  [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} {a a₁ a₂ : α} {b b₁ b₂ : β}
+  [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι}
 
 lemma monovaryOn_iff_forall_smul_nonneg :
     MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i) := by
@@ -380,7 +380,7 @@ alias ⟨AntivaryOn.smul_add_smul_le_smul_add_smul, _⟩ := antivaryOn_iff_smul_
 end LinearOrderedAddCommGroup
 
 section LinearOrderedRing
-variable [LinearOrderedRing α] {f g : ι → α} {s : Set ι} {a b c d : α}
+variable [LinearOrderedRing α] {f g : ι → α} {s : Set ι}
 
 lemma monovaryOn_iff_forall_mul_nonneg :
     MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i) := by

Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean

@@ -273,13 +273,6 @@ def coeRingHom : { x : α // 0 ≤ x } →+* α :=
 
 end Semiring
 
-section Nontrivial
-
-variable [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
-  [CovariantClass α α (· + ·) (· ≤ ·)] [PosMulMono α]
-
-end Nontrivial
-
 section CommSemiring
 
 variable [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α]

Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

@@ -29,7 +29,7 @@ assert_not_exists GaloisConnection
 
 namespace Rat
 
-variable {a b c p q : ℚ}
+variable {a b p q : ℚ}
 
 @[simp] lemma divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a := by
   cases' hab : a /. b with n d hd hnd

Mathlib/Algebra/Ring/Hom/Basic.lean

@@ -21,13 +21,13 @@ They could be moved to more natural homes.
 
 open Function
 
-variable {F α β γ : Type*}
+variable {α β : Type*}
 
 namespace RingHom
 
 section
 
-variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β) {x y : α}
+variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β)
 
 /-- `f : α →+* β` has a trivial codomain iff its range is `{0}`. -/
 theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=

Mathlib/Algebra/Ring/Parity.lean

@@ -31,7 +31,7 @@ assert_not_exists OrderedRing
 
 open MulOpposite
 
-variable {F α β R : Type*}
+variable {F α β : Type*}
 
 section Monoid
 variable [Monoid α] [HasDistribNeg α] {n : ℕ} {a : α}
@@ -156,7 +156,7 @@ lemma Odd.pow_add_pow_eq_zero [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) :
 end Semiring
 
 section Monoid
-variable [Monoid α] [HasDistribNeg α] {a : α} {n : ℕ}
+variable [Monoid α] [HasDistribNeg α] {n : ℕ}
 
 lemma Odd.neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n := by
   rintro ⟨c, rfl⟩ a; simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

@@ -57,7 +57,7 @@ namespace BoxAdditiveMap
 
 open Box Prepartition Finset
 
-variable {N : Type*} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (Box ι)} {I J : Box ι}
+variable {N : Type*} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (Box ι)} {I : Box ι}
   {i : ι}
 
 instance : FunLike (ι →ᵇᵃ[I₀] M) (Box ι) M where

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -97,7 +97,6 @@ open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
 
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
 variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 /-- `f` has the derivative `f'` at the point `x` as `x` goes along the filter `L`.
 
@@ -142,7 +141,7 @@ If the derivative exists (i.e., `∃ f', HasDerivAt f f' x`), then
 def deriv (f : 𝕜 → F) (x : 𝕜) :=
   fderiv 𝕜 f x 1
 
-variable {f f₀ f₁ g : 𝕜 → F}
+variable {f f₀ f₁ : 𝕜 → F}
 variable {f' f₀' f₁' g' : F}
 variable {x : 𝕜}
 variable {s t : Set 𝕜}

Mathlib/Analysis/Calculus/Deriv/Comp.lean

@@ -43,11 +43,11 @@ open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
 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 {f : 𝕜 → F}
+variable {f' : F}
 variable {x : 𝕜}
-variable {s t : Set 𝕜}
-variable {L L₁ L₂ : Filter 𝕜}
+variable {s : Set 𝕜}
+variable {L : Filter 𝕜}
 
 section Composition
 
@@ -65,8 +65,8 @@ usual multiplication in `comp` lemmas.
 /- For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to
 get confused since there are too many possibilities for composition -/
 variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F]
-  [IsScalarTower 𝕜 𝕜' F] {s' t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₁ : 𝕜 → 𝕜} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}
-  {h₁' : 𝕜} {g₁ : 𝕜' → F} {g₁' : F} {L' : Filter 𝕜'} {y : 𝕜'} (x)
+  [IsScalarTower 𝕜 𝕜' F] {s' t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}
+  {g₁ : 𝕜' → F} {g₁' : F} {L' : Filter 𝕜'} {y : 𝕜'} (x)
 
 theorem HasDerivAtFilter.scomp (hg : HasDerivAtFilter g₁ g₁' (h x) L')
     (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :

Mathlib/Analysis/Calculus/Deriv/Inv.lean

@@ -21,21 +21,14 @@ derivative
 -/
 
 
-universe u v w
+universe u
 
-open scoped Classical Topology ENNReal
+open scoped Topology
 open Filter Asymptotics Set
 
-open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
+open ContinuousLinearMap (smulRight)
 
-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 {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜}
 
 section Inverse
 
@@ -101,7 +94,7 @@ theorem fderivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s
   rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]
   exact fderiv_inv
 
-variable {c : 𝕜 → 𝕜} {h : E → 𝕜} {c' : 𝕜} {z : E} {S : Set E}
+variable {c : 𝕜 → 𝕜} {c' : 𝕜}
 
 theorem HasDerivWithinAt.inv (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) :
     HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x := by

Mathlib/Analysis/Calculus/Deriv/Polynomial.lean

@@ -28,21 +28,13 @@ derivative, polynomial
 -/
 
 
-universe u v w
+universe u
 
-open scoped Topology Filter ENNReal Polynomial
-open Set
+open scoped Polynomial
 
-open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
+open ContinuousLinearMap (smulRight)
 
-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 L₁ L₂ : Filter 𝕜}
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜}
 
 namespace Polynomial
 

Mathlib/Analysis/Calculus/Deriv/Pow.lean

@@ -19,21 +19,9 @@ For a more detailed overview of one-dimensional derivatives in mathlib, see the
 derivative, power
 -/
 
-universe u v w
+universe u
 
-open scoped Classical
-open Topology Filter ENNReal
-
-open Filter 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 L₁ L₂ : Filter 𝕜}
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜}
 
 /-! ### Derivative of `x ↦ x^n` for `n : ℕ` -/
 

Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean

@@ -16,9 +16,7 @@ bounded bilinear maps.
 -/
 
 
-open Filter Asymptotics ContinuousLinearMap Set Metric
-open scoped Classical
-open Topology NNReal Asymptotics ENNReal
+open Asymptotics Topology
 
 noncomputable section
 
@@ -29,12 +27,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
-variable {f f₀ f₁ g : E → F}
-variable {f' f₀' f₁' g' : E →L[𝕜] F}
-variable (e : E →L[𝕜] F)
-variable {x : E}
-variable {s t : Set E}
-variable {L L₁ L₂ : Filter E}
 
 section BilinearMap
 

Mathlib/Analysis/Calculus/FDeriv/Linear.lean

@@ -17,26 +17,18 @@ bounded linear maps.
 -/
 
 
-open Filter Asymptotics ContinuousLinearMap Set Metric
-
-open scoped Classical
-open Topology NNReal Filter Asymptotics ENNReal
-
-noncomputable section
+open Asymptotics
 
 section
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
-variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
-variable {f f₀ f₁ g : E → F}
-variable {f' f₀' f₁' g' : E →L[𝕜] F}
+variable {f : E → F}
 variable (e : E →L[𝕜] F)
 variable {x : E}
-variable {s t : Set E}
-variable {L L₁ L₂ : Filter E}
+variable {s : Set E}
+variable {L : Filter E}
 
 section ContinuousLinearMap
 

Mathlib/Analysis/Convex/EGauge.lean

@@ -65,8 +65,7 @@ end SMul
 
 section SMulZero
 
-variable (𝕜 : Type*) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type*} [Zero E] [SMulZeroClass 𝕜 E]
-  {c : 𝕜} {s t : Set E} {x : E} {r : ℝ≥0∞}
+variable (𝕜 : Type*) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type*} [Zero E] [SMulZeroClass 𝕜 E] {x : E}
 
 @[simp] lemma egauge_zero_left_eq_top : egauge 𝕜 0 x = ∞ ↔ x ≠ 0 := by
   simp [egauge_eq_top]
@@ -77,8 +76,8 @@ end SMulZero
 
 section Module
 
-variable {𝕜 : Type*} [NormedDivisionRing 𝕜] {α E : Type*} [AddCommGroup E] [Module 𝕜 E]
-    {c : 𝕜} {s t : Set E} {x y : E} {r : ℝ≥0∞}
+variable {𝕜 : Type*} [NormedDivisionRing 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+    {c : 𝕜} {s : Set E} {x : E}
 
 /-- If `c • x ∈ s` and `c ≠ 0`, then `egauge 𝕜 s x` is at most `((‖c‖₊⁻¹ : ℝ≥0) : ℝ≥0∞).
 
@@ -159,8 +158,7 @@ end Module
 
 section SeminormedAddCommGroup
 
-variable (𝕜 : Type*) [NormedField 𝕜] {α E : Type*}
-    [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} {s t : Set E} {x y : E}
+variable (𝕜 : Type*) [NormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 lemma div_le_egauge_closedBall (r : ℝ≥0) (x : E) : ‖x‖₊ / r ≤ egauge 𝕜 (closedBall 0 r) x := by
   rw [le_egauge_iff]
@@ -183,8 +181,8 @@ end SeminormedAddCommGroup
 
 section SeminormedAddCommGroup
 
-variable {𝕜 : Type*} [NormedField 𝕜] {α E : Type*}
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} {s t : Set E} {x y : E} {r : ℝ≥0}
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} {x : E} {r : ℝ≥0}
 
 lemma egauge_ball_le_of_one_lt_norm (hc : 1 < ‖c‖) (h₀ : r ≠ 0 ∨ x ≠ 0) :
     egauge 𝕜 (ball 0 r) x ≤ ‖c‖₊ * ‖x‖₊ / r := by