chore: remove unused variables (#19413)

#17715
leanprover-community · Nov 25, 2024 · c4f3076 · c4f3076
1 parent a3580b7
commit c4f3076
Show file tree

Hide file tree

Showing 54 changed files with 83 additions and 106 deletions.
diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@@ -38,7 +38,7 @@ lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
 end Mul
 
 section InvolutiveInv
-variable [InvolutiveInv G] {s t : Set G}
+variable [InvolutiveInv G]
 
 @[to_additive (attr := simp)]
 lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by

diff --git a/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean b/Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean
@@ -13,7 +13,7 @@ import Mathlib.SetTheory.Cardinal.Finite
 
 open scoped Cardinal Pointwise
 
-variable {G G₀ M M₀ : Type*}
+variable {G₀ M₀ : Type*}
 
 namespace Set
 variable [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀}

diff --git a/Mathlib/Algebra/Homology/Additive.lean b/Mathlib/Algebra/Homology/Additive.lean
@@ -23,8 +23,8 @@ variable {ι : Type*}
 variable {V : Type u} [Category.{v} V] [Preadditive V]
 variable {W : Type*} [Category W] [Preadditive W]
 variable {W₁ W₂ : Type*} [Category W₁] [Category W₂] [HasZeroMorphisms W₁] [HasZeroMorphisms W₂]
-variable {c : ComplexShape ι} {C D E : HomologicalComplex V c}
-variable (f g : C ⟶ D) (h k : D ⟶ E) (i : ι)
+variable {c : ComplexShape ι} {C D : HomologicalComplex V c}
+variable (f : C ⟶ D) (i : ι)
 
 namespace HomologicalComplex
 

diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -93,7 +93,7 @@ theorem equivTuple_apply {R : Type*} (c₁ c₂ : R) (x : ℍ[R,c₁,c₂]) :
 @[simp]
 theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a.4 = a := rfl
 
-variable {S T R : Type*} {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂])
+variable {S T R : Type*} {c₁ c₂ : R} (r x y : R) (a b : ℍ[R,c₁,c₂])
 
 instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton
 instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial
@@ -742,7 +742,7 @@ instance {R : Type*} [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R] :=
 
 namespace Quaternion
 
-variable {S T R : Type*} [CommRing R] (r x y z : R) (a b c : ℍ[R])
+variable {S T R : Type*} [CommRing R] (r x y : R) (a b : ℍ[R])
 
 export QuaternionAlgebra (re imI imJ imK)
 

diff --git a/Mathlib/Algebra/TrivSqZeroExt.lean b/Mathlib/Algebra/TrivSqZeroExt.lean
@@ -870,10 +870,9 @@ section Algebra
 
 variable (S : Type*) (R R' : Type u) (M : Type v)
 variable [CommSemiring S] [Semiring R] [CommSemiring R'] [AddCommMonoid M]
-variable [Algebra S R] [Algebra S R'] [Module S M]
-variable [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+variable [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
 variable [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M]
-variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] [IsScalarTower S R' M]
+variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]
 
 instance algebra' : Algebra S (tsze R M) :=
   { (TrivSqZeroExt.inlHom R M).comp (algebraMap S R) with

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@@ -142,8 +142,7 @@ instance inf (P Q : MorphismProperty Scheme) [IsLocalAtTarget P] [IsLocalAtTarge
      fun h ↦ ⟨(iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).left),
       (iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).right)⟩⟩
 
-variable {P} [hP : IsLocalAtTarget P]
-variable {X Y U V : Scheme.{u}} {f : X ⟶ Y} {g : U ⟶ Y} [IsOpenImmersion g] (𝒰 : Y.OpenCover)
+variable {P} [hP : IsLocalAtTarget P] {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : Y.OpenCover)
 
 lemma of_isPullback {UX UY : Scheme.{u}} {iY : UY ⟶ Y} [IsOpenImmersion iY]
     {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : IsPullback iX f' f iY) (H : P f) : P f' := by
@@ -228,7 +227,7 @@ instance inf (P Q : MorphismProperty Scheme) [IsLocalAtSource P] [IsLocalAtSourc
       (iff_of_openCover' f 𝒰).mpr (fun i ↦ (h i).right)⟩⟩
 
 variable {P} [IsLocalAtSource P]
-variable {X Y U V : Scheme.{u}} {f : X ⟶ Y} {g : U ⟶ Y} [IsOpenImmersion g] (𝒰 : X.OpenCover)
+variable {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : X.OpenCover)
 
 lemma comp {UX : Scheme.{u}} (H : P f) (i : UX ⟶ X) [IsOpenImmersion i] :
     P (i ≫ f) :=

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean b/Mathlib/AlgebraicGeometry/Morphisms/Etale.lean
@@ -28,7 +28,7 @@ abbrev IsEtale {X Y : Scheme.{u}} (f : X ⟶ Y) := IsSmoothOfRelativeDimension 0
 
 namespace IsEtale
 
-variable {X Y : Scheme.{u}} (f : X ⟶ Y)
+variable {X : Scheme.{u}}
 
 instance : IsStableUnderBaseChange @IsEtale :=
   isSmoothOfRelativeDimension_isStableUnderBaseChange 0

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
@@ -26,7 +26,7 @@ universe u
 
 namespace AlgebraicGeometry
 
-variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
+variable {X Y : Scheme.{u}}
 
 theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} : IsOpenImmersion f ↔
     IsOpenEmbedding f.base ∧ ∀ x, IsIso (f.stalkMap x) := by

diff --git a/Mathlib/AlgebraicGeometry/SpreadingOut.lean b/Mathlib/AlgebraicGeometry/SpreadingOut.lean
@@ -49,8 +49,7 @@ open CategoryTheory
 
 namespace AlgebraicGeometry
 
-variable {X Y S : Scheme.{u}} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (e : f ≫ sY = sX)
-variable {R A : CommRingCat.{u}}
+variable {X Y S : Scheme.{u}} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) {R A : CommRingCat.{u}}
 
 /-- The germ map at `x` is injective if there exists some affine `U ∋ x`
   such that the map `Γ(X, U) ⟶ X_x` is injective -/

diff --git a/Mathlib/Analysis/Convex/Gauge.lean b/Mathlib/Analysis/Convex/Gauge.lean
@@ -41,7 +41,7 @@ open scoped Pointwise Topology NNReal
 
 noncomputable section
 
-variable {𝕜 E F : Type*}
+variable {𝕜 E : Type*}
 
 section AddCommGroup
 

diff --git a/Mathlib/Analysis/Convex/Normed.lean b/Mathlib/Analysis/Convex/Normed.lean
@@ -25,14 +25,14 @@ We prove the following facts:
   is bounded.
 -/
 
-variable {ι : Type*} {E P : Type*}
+variable {E P : Type*}
 
 open AffineBasis Module Metric Set
 open scoped Convex Pointwise Topology
 
 section SeminormedAddCommGroup
 variable [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P]
-variable {s t : Set E}
+variable {s : Set E}
 
 /-- The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn`
 and `convexOn_univ_norm`. -/

diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -1600,9 +1600,7 @@ end ContinuousLinearMap
 
 section
 
-variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
-variable {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
-variable {E'' : Type*} [SeminormedAddCommGroup E''] [InnerProductSpace 𝕜 E'']
+variable {ι : Type*} {ι' : Type*} {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
 
 @[simp]
 theorem Orthonormal.equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
@@ -1683,7 +1681,7 @@ open scoped InnerProductSpace
 
 variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
-variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
+variable {ι : Type*}
 
 local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 
@@ -2188,9 +2186,7 @@ local notation "IK" => @RCLike.I 𝕜 _
 
 local postfix:90 "†" => starRingEnd _
 
-variable {ι : Type*}
-variable {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)] [∀ i, InnerProductSpace 𝕜 (G i)]
-  {V : ∀ i, G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [dec_V : ∀ (i) (x : G i), Decidable (x ≠ 0)]
+variable {ι : Type*} {G : ι → Type*}
 
 /-- An orthogonal family forms an independent family of subspaces; that is, any collection of
 elements each from a different subspace in the family is linearly independent. In particular, the

diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -955,7 +955,7 @@ theorem NormedAddCommGroup.tendsto_atTop' [Nonempty α] [Preorder α] [IsDirecte
 
 section RingHomIsometric
 
-variable {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
+variable {R₁ R₂ : Type*}
 
 /-- This class states that a ring homomorphism is isometric. This is a sufficient assumption
 for a continuous semilinear map to be bounded and this is the main use for this typeclass. -/
@@ -965,7 +965,7 @@ class RingHomIsometric [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (
 
 attribute [simp] RingHomIsometric.is_iso
 
-variable [SeminormedRing R₁] [SeminormedRing R₂] [SeminormedRing R₃]
+variable [SeminormedRing R₁]
 
 instance RingHomIsometric.ids : RingHomIsometric (RingHom.id R₁) :=
   ⟨rfl⟩

diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -44,7 +44,7 @@ normed group
 -/
 
 
-variable {𝓕 𝕜 α ι κ E F G : Type*}
+variable {𝓕 α ι κ E F G : Type*}
 
 open Filter Function Metric Bornology
 
@@ -337,7 +337,7 @@ abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommG
 section SeminormedGroup
 
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b b₁ b₂ c : E} {r r₁ r₂ : ℝ}
+  {a a₁ a₂ b c : E} {r r₁ r₂ : ℝ}
 
 @[to_additive]
 theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ :=
@@ -1024,7 +1024,7 @@ end Induced
 
 section SeminormedCommGroup
 
-variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a b : E} {r : ℝ}
 
 @[to_additive]
 theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹ := by
@@ -1290,7 +1290,7 @@ end SeminormedCommGroup
 
 section NormedGroup
 
-variable [NormedGroup E] [NormedGroup F] {a b : E}
+variable [NormedGroup E] {a b : E}
 
 @[to_additive (attr := simp) norm_eq_zero]
 theorem norm_eq_zero'' : ‖a‖ = 0 ↔ a = 1 :=

diff --git a/Mathlib/Analysis/Normed/Group/Bounded.lean b/Mathlib/Analysis/Normed/Group/Bounded.lean
@@ -21,11 +21,10 @@ normed group
 open Filter Metric Bornology
 open scoped Pointwise Topology
 
-variable {α ι E F G : Type*}
+variable {α E F G : Type*}
 
 section SeminormedGroup
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
 
 @[to_additive (attr := simp) comap_norm_atTop]
 lemma comap_norm_atTop' : comap norm atTop = cobounded E := by

diff --git a/Mathlib/Analysis/Normed/Group/Uniform.lean b/Mathlib/Analysis/Normed/Group/Uniform.lean
@@ -15,13 +15,13 @@ This file proves lipschitzness of normed group operations and shows that normed
 groups.
 -/
 
-variable {𝓕 α E F : Type*}
+variable {𝓕 E F : Type*}
 
 open Filter Function Metric Bornology
 open scoped ENNReal NNReal Uniformity Pointwise Topology
 
 section SeminormedGroup
-variable [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a b : E} {r : ℝ}
 
 @[to_additive]
 instance NormedGroup.to_isometricSMul_right : IsometricSMul Eᵐᵒᵖ E :=
@@ -177,7 +177,7 @@ end SeminormedGroup
 
 section SeminormedCommGroup
 
-variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
+variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ}
 
 @[to_additive]
 instance NormedGroup.to_isometricSMul_left : IsometricSMul E E :=
@@ -239,7 +239,7 @@ theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
 
 section PseudoEMetricSpace
 variable {α E : Type*} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0}
-  {f g : α → E} {s : Set α} {x : α}
+  {f g : α → E} {s : Set α}
 
 @[to_additive (attr := simp)]
 lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith]

diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -54,8 +54,7 @@ namespace LinearIsometry
 
 open LinearMap
 
-variable {R : Type*} [Semiring R]
-variable {F E₁ : Type*} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] [Module R E₁]
+variable {F E₁ : Type*} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁]
 variable {R₁ : Type*} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁]
   [FiniteDimensional R₁ F]
 
@@ -110,9 +109,7 @@ end AffineIsometry
 section CompleteField
 
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type x}
-  [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F']
-  [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜]
+  [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜]
 
 section Affine
 

diff --git a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean
@@ -22,7 +22,6 @@ open CategoryTheory.Limits
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-  (E : Type u₃) [Category.{v₃} E]
 
 noncomputable section
 

diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean
@@ -316,7 +316,7 @@ lemma hasMap_of_iso (e : X ≅ Y) (p: I → J) [HasMap X p] : HasMap Y p := fun
   exact hasColimitOfIso α.symm
 
 section
-variable [X.HasMap p] [Y.HasMap p] [Z.HasMap p]
+variable [X.HasMap p] [Y.HasMap p]
 
 /-- Given `X : GradedObject I C` and `p : I → J`, `X.mapObj p` is the graded object by `J`
 which in degree `j` consists of the coproduct of the `X i` such that `p i = j`. -/

diff --git a/Mathlib/CategoryTheory/GuitartExact/Basic.lean b/Mathlib/CategoryTheory/GuitartExact/Basic.lean
@@ -128,7 +128,6 @@ abbrev CostructuredArrowDownwards.mk (comm : R.map a ≫ w.app X₁ ≫ B.map b
   CostructuredArrow.mk (Y := StructuredArrow.mk a)
     (StructuredArrow.homMk b (by simpa using comm))
 
-variable (comm : R.map a ≫ w.app X₁ ≫ B.map b = g)
 variable {w g}
 
 lemma StructuredArrowRightwards.mk_surjective

diff --git a/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean b/Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
@@ -48,7 +48,7 @@ variable {C : Type u} [Category.{v} C]
 
 namespace PresheafOfGroups
 
-variable (G : Cᵒᵖ ⥤ Grp.{w}) {X : C} {I : Type w'} (U : I → C)
+variable (G : Cᵒᵖ ⥤ Grp.{w}) {I : Type w'} (U : I → C)
 
 /-- A zero cochain consists of a family of sections. -/
 def ZeroCochain := ∀ (i : I), G.obj (Opposite.op (U i))

diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@@ -34,8 +34,7 @@ open Fintype (card)
 
 namespace SimpleGraph
 
-variable {α β 𝕜 : Type*} [LinearOrderedField 𝕜] {G H : SimpleGraph α} {ε δ : 𝕜} {n : ℕ}
-  {s : Finset α}
+variable {α β 𝕜 : Type*} [LinearOrderedField 𝕜] {G H : SimpleGraph α} {ε δ : 𝕜}
 
 section LocallyLinear
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
@@ -23,7 +23,7 @@ attribute [-instance] decidableEq_of_subsingleton
 
 open Finset Fintype
 
-variable {α : Type*} (G G' : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α}
+variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α}
 
 namespace SimpleGraph
 
@@ -146,7 +146,7 @@ private lemma triple_eq_triple_of_mem (hst : Disjoint s t) (hsu : Disjoint s u)
   · rintro rfl
     solve_by_elim
 
-variable [Fintype α] {P : Finpartition (univ : Finset α)}
+variable [Fintype α]
 
 /-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are disjoint sets of
 vertices such that each pair is `ε`-uniform and `2 * ε`-dense, then `G` contains at least

diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@@ -38,7 +38,7 @@ This construction shows up unrelatedly twice in the theory of Roth numbers:
 open Finset Function Sum3
 
 variable {α β γ 𝕜 : Type*} [LinearOrderedField 𝕜] {t : Finset (α × β × γ)} {a a' : α} {b b' : β}
-  {c c' : γ} {x : α × β × γ} {ε : 𝕜}
+  {c c' : γ} {x : α × β × γ}
 
 namespace SimpleGraph
 namespace TripartiteFromTriangles

diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
@@ -311,8 +311,6 @@ end Mathlib.Meta.Positivity
 
 namespace Real
 
-variable {x y : ℝ}
-
 @[simp]
 theorem sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x * y) = √x * √y := by
   simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]

diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -80,7 +80,7 @@ theorem isPiSystem_pi [∀ i, MeasurableSpace (α i)] :
 
 section Finite
 
-variable [Finite ι] [Finite ι']
+variable [Finite ι]
 
 /-- Boxes of countably spanning sets are countably spanning. -/
 theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :

diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean
@@ -28,7 +28,7 @@ namespace MeasureTheory
 
 universe u v w
 
-variable {G : Type u} {M : Type v} {α : Type w} {s : Set α}
+variable {G : Type u} {M : Type v} {α : Type w}
 
 namespace SMulInvariantMeasure
 
@@ -198,7 +198,7 @@ instance smulInvariantMeasure_map_smul [SMul M α] [SMul N α] [SMulCommClass N
 
 end SMulHomClass
 
-variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] (c : G) (μ : Measure α)
+variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure α)
 
 variable [MeasurableSpace G] [MeasurableSMul G α] in
 /-- Equivalent definitions of a measure invariant under a multiplicative action of a group.