[Merged by Bors] - style: remove redundant instance arguments

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2269,7 +2269,7 @@ lemma prod_of_injective (e : ι → κ) (hf : Injective e) (f : ι → α) (g :
   prod_of_injOn e (hf.injOn _) (by simp) (by simpa using h') (fun i _ ↦ h i)
 
 @[to_additive]
-lemma prod_fiberwise [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : ι → α) :
+lemma prod_fiberwise [DecidableEq κ] (g : ι → κ) (f : ι → α) :
     ∏ j, ∏ i : {i // g i = j}, f i = ∏ i, f i := by
   rw [← Finset.prod_fiberwise _ g f]
   congr with j
@@ -2278,7 +2278,7 @@ lemma prod_fiberwise [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : ι → 
 #align fintype.sum_fiberwise Fintype.sum_fiberwise
 
 @[to_additive]
-lemma prod_fiberwise' [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : κ → α) :
+lemma prod_fiberwise' [DecidableEq κ] (g : ι → κ) (f : κ → α) :
     ∏ j, ∏ _i : {i // g i = j}, f j = ∏ i, f (g i) := by
   rw [← Finset.prod_fiberwise' _ g f]
   congr with j

Mathlib/Algebra/CharP/Basic.lean

@@ -388,7 +388,7 @@ theorem ringChar_ne_zero_of_finite [Finite R] : ringChar R ≠ 0 :=
   char_ne_zero_of_finite R (ringChar R)
 #align char_p.ring_char_ne_zero_of_finite CharP.ringChar_ne_zero_of_finite
 
-theorem ringChar_zero_iff_CharZero [NonAssocRing R] : ringChar R = 0 ↔ CharZero R := by
+theorem ringChar_zero_iff_CharZero : ringChar R = 0 ↔ CharZero R := by
   rw [ringChar.eq_iff, charP_zero_iff_charZero]
 
 end

Mathlib/Algebra/Group/Hom/Basic.lean

@@ -190,7 +190,7 @@ lemma mul_comp [MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) :
 #align add_monoid_hom.add_comp AddMonoidHom.add_comp
 
 @[to_additive]
-lemma comp_mul [CommMonoid N] [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
+lemma comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
     g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
   ext; simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
 #align monoid_hom.comp_mul MonoidHom.comp_mul

Mathlib/Algebra/Group/NatPowAssoc.lean

@@ -95,7 +95,7 @@ section Monoid
 
 variable [Monoid M]
 
-instance Monoid.PowAssoc [Monoid M] : NatPowAssoc M where
+instance Monoid.PowAssoc : NatPowAssoc M where
   npow_add _ _ _ := pow_add _ _ _
   npow_zero _ := pow_zero _
   npow_one _ := pow_one _

Mathlib/Algebra/Group/Units.lean

@@ -705,7 +705,7 @@ lemma IsUnit.exists_right_inv (h : IsUnit a) : ∃ b, a * b = 1 := by
 #align is_add_unit.exists_neg IsAddUnit.exists_neg
 
 @[to_additive IsAddUnit.exists_neg']
-lemma IsUnit.exists_left_inv [Monoid M] {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by
+lemma IsUnit.exists_left_inv {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by
   rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
   exact ⟨b, hba⟩
 #align is_unit.exists_left_inv IsUnit.exists_left_inv

Mathlib/Algebra/Module/Submodule/Localization.lean

@@ -30,7 +30,7 @@ open nonZeroDivisors
 universe u u' v v'
 
 variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
-variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M]
+variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
 variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
 variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
 variable (hp : p ≤ R⁰)

Mathlib/Algebra/Order/Group/Abs.lean

@@ -183,7 +183,7 @@ lemma inf_sq_eq_mul_div_mabs_div (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ
 -- See, e.g. Zaanen, Lectures on Riesz Spaces
 -- 3rd lecture
 @[to_additive]
-lemma mabs_div_sup_mul_mabs_div_inf [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
+lemma mabs_div_sup_mul_mabs_div_inf (a b c : α) :
     |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ := by
   letI : DistribLattice α := CommGroup.toDistribLattice α
   calc

Mathlib/Algebra/Order/Group/Lattice.lean

@@ -93,7 +93,7 @@ lemma inf_div (a b c : α) : (a ⊓ b) / c = a / c ⊓ b / c := (OrderIso.divRig
 -- Chapter V, 1.E
 -- See also `one_le_pow_iff` for the existing version in linear orders
 @[to_additive]
-lemma pow_two_semiclosed [CovariantClass α α (· * ·) (· ≤ ·)]
+lemma pow_two_semiclosed
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a := by
   suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
     rwa [← inf_eq_right, ← mul_right_eq_self]

Mathlib/Algebra/Order/Module/OrderedSMul.lean

@@ -65,8 +65,7 @@ instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where
 instance OrderedSMul.toPosSMulReflectLT : PosSMulReflectLT R M :=
   PosSMulReflectLT.of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha
 
-instance OrderDual.instOrderedSMul [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M]
-    [OrderedSMul R M] : OrderedSMul R Mᵒᵈ where
+instance OrderDual.instOrderedSMul : OrderedSMul R Mᵒᵈ where
   smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M)
   lt_of_smul_lt_smul_of_pos := OrderedSMul.lt_of_smul_lt_smul_of_pos (M := M)
 

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -487,7 +487,7 @@ lemma one_eq_coe : 1 = (a : WithBot α) ↔ a = 1 := eq_comm.trans coe_eq_one
 @[to_additive (attr := simp)] lemma one_ne_bot : (1 : WithBot α) ≠ ⊥ := coe_ne_bot
 
 @[to_additive (attr := simp)]
-theorem unbot_one [One α] : (1 : WithBot α).unbot coe_ne_bot = 1 :=
+theorem unbot_one : (1 : WithBot α).unbot coe_ne_bot = 1 :=
   rfl
 #align with_bot.unbot_one WithBot.unbot_one
 #align with_bot.unbot_zero WithBot.unbot_zero

Mathlib/Algebra/Star/Subalgebra.lean

@@ -745,7 +745,7 @@ theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (h
   DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial
 #align star_alg_hom.ext_of_adjoin_eq_top StarAlgHom.ext_of_adjoin_eq_top
 
-theorem map_adjoin [StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A) :
+theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) :
     map f (adjoin R s) = adjoin R (f '' s) :=
   GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarSubalgebra.gc
     StarSubalgebra.gc fun _ => rfl

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -514,25 +514,25 @@ theorem eq_orthogonalProjection_of_mem_of_inner_eq_zero {u v : E} (hvm : v ∈ K
 
 /-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
 orthogonal projection. -/
-theorem eq_orthogonalProjection_of_mem_orthogonal [HasOrthogonalProjection K] {u v : E} (hv : v ∈ K)
+theorem eq_orthogonalProjection_of_mem_orthogonal {u v : E} (hv : v ∈ K)
     (hvo : u - v ∈ Kᗮ) : (orthogonalProjection K u : E) = v :=
   eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hv <| (Submodule.mem_orthogonal' _ _).1 hvo
 #align eq_orthogonal_projection_of_mem_orthogonal eq_orthogonalProjection_of_mem_orthogonal
 
 /-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
 orthogonal projection. -/
-theorem eq_orthogonalProjection_of_mem_orthogonal' [HasOrthogonalProjection K] {u v z : E}
+theorem eq_orthogonalProjection_of_mem_orthogonal' {u v z : E}
     (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) : (orthogonalProjection K u : E) = v :=
   eq_orthogonalProjection_of_mem_orthogonal hv (by simpa [hu] )
 #align eq_orthogonal_projection_of_mem_orthogonal' eq_orthogonalProjection_of_mem_orthogonal'
 
 @[simp]
-theorem orthogonalProjection_orthogonal_val [HasOrthogonalProjection K] (u : E) :
+theorem orthogonalProjection_orthogonal_val (u : E) :
     (orthogonalProjection Kᗮ u : E) = u - orthogonalProjection K u :=
   eq_orthogonalProjection_of_mem_orthogonal' (sub_orthogonalProjection_mem_orthogonal _)
     (K.le_orthogonal_orthogonal (orthogonalProjection K u).2) <| by simp
 
-theorem orthogonalProjection_orthogonal [HasOrthogonalProjection K] (u : E) :
+theorem orthogonalProjection_orthogonal (u : E) :
     orthogonalProjection Kᗮ u =
       ⟨u - orthogonalProjection K u, sub_orthogonalProjection_mem_orthogonal _⟩ :=
   Subtype.eq <| orthogonalProjection_orthogonal_val _

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -49,6 +49,7 @@ attribute [inherit_doc NormedSpace] NormedSpace.norm_smul_le
 end Prio
 
 variable [NormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]
+variable [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]
 
 -- see Note [lower instance priority]
 instance (priority := 100) NormedSpace.boundedSMul [NormedSpace 𝕜 E] : BoundedSMul 𝕜 E :=
@@ -68,9 +69,6 @@ theorem norm_zsmul [NormedSpace 𝕜 E] (n : ℤ) (x : E) : ‖n • x‖ = ‖(
   rw [← norm_smul, ← Int.smul_one_eq_coe, smul_assoc, one_smul]
 #align norm_zsmul norm_zsmul
 
-variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-variable [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
-
 theorem eventually_nhds_norm_smul_sub_lt (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) :
     ∀ᶠ y in 𝓝 x, ‖c • (y - x)‖ < ε :=
   have : Tendsto (fun y ↦ ‖c • (y - x)‖) (𝓝 x) (𝓝 0) :=

Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean

@@ -59,7 +59,7 @@ section Abelian
 
 variable [Abelian C]
 
-lemma exact₀ [Abelian C] {Z : C} (P : ProjectiveResolution Z) :
+lemma exact₀ {Z : C} (P : ProjectiveResolution Z) :
     (ShortComplex.mk _ _ P.complex_d_comp_π_f_zero).Exact :=
   ShortComplex.exact_of_g_is_cokernel _ P.isColimitCokernelCofork
 

Mathlib/CategoryTheory/Preadditive/Biproducts.lean

@@ -271,7 +271,7 @@ theorem biproduct.matrix_desc [Fintype K] {f : J → C} {g : K → C}
   simp [lift_desc]
 #align category_theory.limits.biproduct.matrix_desc CategoryTheory.Limits.biproduct.matrix_desc
 
-variable [Finite K] [HasFiniteBiproducts C]
+variable [Finite K]
 
 @[reassoc]
 theorem biproduct.matrix_map {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k)

Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean

@@ -24,7 +24,7 @@ namespace CategoryTheory
 variable {C : Type*} [Category C] [Precoherent C]
 
 universe w in
-lemma isSheaf_coherent [Precoherent C] (P : Cᵒᵖ ⥤ Type w) :
+lemma isSheaf_coherent (P : Cᵒᵖ ⥤ Type w) :
     Presieve.IsSheaf (coherentTopology C) P ↔
     (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → (X a ⟶ B)),
       EffectiveEpiFamily X π → (Presieve.ofArrows X π).IsSheafFor P) := by

Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

@@ -44,7 +44,7 @@ theorem precoherent : Precoherent D where
       infer_instance
     · simpa using congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map) (h' b)
 
-instance [EssentiallySmall C] [Precoherent C] :
+instance [EssentiallySmall C] :
     Precoherent (SmallModel C) := (equivSmallModel C).precoherent
 
 /--
@@ -124,7 +124,7 @@ theorem preregular : Preregular D where
       e.functor.map i' ≫ e.counit.app _, ?_⟩
     simpa using congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map) w
 
-instance [EssentiallySmall C] [Preregular C] :
+instance [EssentiallySmall C] :
     Preregular (SmallModel C) := (equivSmallModel C).preregular
 
 /--

Mathlib/Data/DFinsupp/Multiset.lean

@@ -124,7 +124,7 @@ namespace DFinsupp
 variable [DecidableEq α] {f g : Π₀ _a : α, ℕ}
 
 @[simp]
-theorem toMultiset_toDFinsupp [DecidableEq α] (f : Π₀ _ : α, ℕ) :
+theorem toMultiset_toDFinsupp (f : Π₀ _ : α, ℕ) :
     Multiset.toDFinsupp (DFinsupp.toMultiset f) = f :=
   Multiset.equivDFinsupp.apply_symm_apply f
 #align dfinsupp.to_multiset_to_dfinsupp DFinsupp.toMultiset_toDFinsupp

Mathlib/Data/Finsupp/WellFounded.lean

@@ -59,17 +59,17 @@ instance Lex.wellFoundedLT {α N} [LT α] [IsTrichotomous α (· < ·)] [hα : W
 
 variable (r)
 
-theorem Lex.wellFounded_of_finite [IsStrictTotalOrder α r] [Finite α] [Zero N]
+theorem Lex.wellFounded_of_finite [IsStrictTotalOrder α r] [Finite α]
     (hs : WellFounded s) : WellFounded (Finsupp.Lex r s) :=
   InvImage.wf (@equivFunOnFinite α N _ _) (Pi.Lex.wellFounded r fun _ => hs)
 #align finsupp.lex.well_founded_of_finite Finsupp.Lex.wellFounded_of_finite
 
-theorem Lex.wellFoundedLT_of_finite [LinearOrder α] [Finite α] [Zero N] [LT N]
+theorem Lex.wellFoundedLT_of_finite [LinearOrder α] [Finite α] [LT N]
     [hwf : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N)) :=
   ⟨Finsupp.Lex.wellFounded_of_finite (· < ·) hwf.1⟩
 #align finsupp.lex.well_founded_lt_of_finite Finsupp.Lex.wellFoundedLT_of_finite
 
-protected theorem wellFoundedLT [Zero N] [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N, ¬n < 0) :
+protected theorem wellFoundedLT [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N, ¬n < 0) :
     WellFoundedLT (α →₀ N) :=
   ⟨InvImage.wf toDFinsupp (DFinsupp.wellFoundedLT fun _ a => hbot a).wf⟩
 #align finsupp.well_founded_lt Finsupp.wellFoundedLT
@@ -79,7 +79,7 @@ instance wellFoundedLT' {N} [CanonicallyOrderedAddCommMonoid N] [WellFoundedLT N
   Finsupp.wellFoundedLT fun a => (zero_le a).not_lt
 #align finsupp.well_founded_lt' Finsupp.wellFoundedLT'
 
-instance wellFoundedLT_of_finite [Finite α] [Zero N] [Preorder N] [WellFoundedLT N] :
+instance wellFoundedLT_of_finite [Finite α] [Preorder N] [WellFoundedLT N] :
     WellFoundedLT (α →₀ N) :=
   ⟨InvImage.wf equivFunOnFinite Function.wellFoundedLT.wf⟩
 #align finsupp.well_founded_lt_of_finite Finsupp.wellFoundedLT_of_finite

Mathlib/Data/Fintype/Sigma.lean

@@ -35,7 +35,7 @@ lemma Set.biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
 lemma Set.biInter_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
     ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesop
 
-variable [Fintype ι] [Π i, Fintype (κ i)]
+variable [Fintype ι]
 
 instance Sigma.instFintype : Fintype (Σ i, κ i) := ⟨univ.sigma fun _ ↦ univ, by simp⟩
 instance PSigma.instFintype : Fintype (Σ' i, κ i) := .ofEquiv _ (Equiv.psigmaEquivSigma _).symm

Mathlib/Data/Int/Order/Basic.lean

@@ -566,7 +566,7 @@ variable [NonAssocRing R] (n r : R)
 lemma bit1_mul : bit1 n * r = (2 : ℤ) • (n * r) + r := by rw [bit1, add_mul, bit0_mul, one_mul]
 #align bit1_mul bit1_mul
 
-lemma mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by
+lemma mul_bit1 {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by
   rw [bit1, mul_add, mul_bit0, mul_one]
 #align mul_bit1 mul_bit1
 

Mathlib/Data/List/EditDistance/Estimator.lean

@@ -133,8 +133,7 @@ instance [∀ a : δ × ℕ, WellFoundedGT { x // x ≤ a }] :
   Estimator.fstInst (Thunk.mk fun _ => _) (Thunk.mk fun _ => _) (estimator' C xs ys)
 
 /-- The initial estimator for Levenshtein distances. -/
-instance [CanonicallyLinearOrderedAddCommMonoid δ]
-    (C : Levenshtein.Cost α β δ) (xs : List α) (ys : List β) :
+instance (C : Levenshtein.Cost α β δ) (xs : List α) (ys : List β) :
     Bot (LevenshteinEstimator C xs ys) where
   bot :=
   { inner :=

Mathlib/Data/Matrix/Basic.lean

@@ -1290,12 +1290,11 @@ theorem scalar_inj [Nonempty n] {r s : α} : scalar n r = scalar n s ↔ r = s :
   (diagonal_injective.comp Function.const_injective).eq_iff
 #align matrix.scalar_inj Matrix.scalar_inj
 
-theorem scalar_commute_iff [Fintype n] [DecidableEq n] {r : α} {M : Matrix n n α} :
+theorem scalar_commute_iff {r : α} {M : Matrix n n α} :
     Commute (scalar n r) M ↔ r • M = MulOpposite.op r • M := by
   simp_rw [Commute, SemiconjBy, scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
 
-theorem scalar_commute [Fintype n] [DecidableEq n] (r : α) (hr : ∀ r', Commute r r')
-    (M : Matrix n n α) :
+theorem scalar_commute (r : α) (hr : ∀ r', Commute r r') (M : Matrix n n α) :
     Commute (scalar n r) M := scalar_commute_iff.2 <| ext fun _ _ => hr _
 #align matrix.scalar.commute Matrix.scalar_commuteₓ
 

Mathlib/Data/Multiset/Basic.lean

@@ -2681,11 +2681,11 @@ theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) :
   rw [inter_comm, replicate_inter, min_comm]
 #align multiset.inter_replicate Multiset.inter_replicate
 
-theorem erase_attach_map_val [DecidableEq α] (s : Multiset α) (x : {x // x ∈ s}) :
+theorem erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) :
     (s.attach.erase x).map (↑) = s.erase x := by
   rw [Multiset.map_erase _ val_injective, attach_map_val]
 
-theorem erase_attach_map [DecidableEq α] (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) :
+theorem erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) :
     (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f := by
   simp only [← Function.comp_apply (f := f)]
   rw [← map_map, erase_attach_map_val]

Mathlib/FieldTheory/Normal.lean

@@ -148,7 +148,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] :
     exact ⟨hp, minpoly.ne_zero hx⟩
 #align normal.of_is_splitting_field Normal.of_isSplittingField
 
-instance Polynomial.SplittingField.instNormal [Field F] (p : F[X]) : Normal F p.SplittingField :=
+instance Polynomial.SplittingField.instNormal (p : F[X]) : Normal F p.SplittingField :=
   Normal.of_isSplittingField p
 #align polynomial.splitting_field.normal Polynomial.SplittingField.instNormal
 

Mathlib/GroupTheory/Exponent.lean

@@ -429,10 +429,10 @@ end Submonoid
 
 section LeftCancelMonoid
 
-variable [LeftCancelMonoid G]
+variable [LeftCancelMonoid G] [Finite G]
 
 @[to_additive]
-theorem ExponentExists.of_finite [Finite G] : ExponentExists G := by
+theorem ExponentExists.of_finite : ExponentExists G := by
   let _inst := Fintype.ofFinite G
   simp only [Monoid.ExponentExists]
   refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
@@ -441,14 +441,13 @@ theorem ExponentExists.of_finite [Finite G] : ExponentExists G := by
     exact order_dvd_exponent g
 
 @[to_additive]
-theorem exponent_ne_zero_of_finite [Finite G] : exponent G ≠ 0 :=
+theorem exponent_ne_zero_of_finite : exponent G ≠ 0 :=
   ExponentExists.of_finite.exponent_ne_zero
 #align monoid.exponent_ne_zero_of_finite Monoid.exponent_ne_zero_of_finite
 #align add_monoid.exponent_ne_zero_of_finite AddMonoid.exponent_ne_zero_of_finite
 
 @[to_additive AddMonoid.one_lt_exponent]
-lemma one_lt_exponent [LeftCancelMonoid G] [Finite G] [Nontrivial G] :
-    1 < Monoid.exponent G := by
+lemma one_lt_exponent [Nontrivial G] : 1 < Monoid.exponent G := by
   rw [Nat.one_lt_iff_ne_zero_and_ne_one]
   exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩
 

Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

@@ -243,7 +243,7 @@ lemma ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
     IsFreeGroup G :=
   (FreeGroupBasis.ofUniqueLift X of h).isFreeGroup
 
-lemma ofMulEquiv [IsFreeGroup G] (e : G ≃* H) : IsFreeGroup H :=
+lemma ofMulEquiv (e : G ≃* H) : IsFreeGroup H :=
   ((basis G).map e).isFreeGroup
 
 end IsFreeGroup

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -311,7 +311,7 @@ theorem orbitRel_conjAct : (orbitRel (ConjAct G) G).Rel = IsConj :=
   funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]
 #align conj_act.orbit_rel_conj_act ConjAct.orbitRel_conjAct
 
-theorem orbit_eq_carrier_conjClasses [Group G] (g : G) :
+theorem orbit_eq_carrier_conjClasses (g : G) :
     orbit (ConjAct G) g = (ConjClasses.mk g).carrier := by
   ext h
   rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

Mathlib/GroupTheory/Perm/ClosureSwap.lean

@@ -126,7 +126,7 @@ theorem closure_of_isSwap_of_isPretransitive [Finite α] {S : Set (Perm α)} (hS
   simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite]
 
 /-- A transitive permutation group generated by transpositions must be the whole symmetric group -/
-theorem surjective_of_isSwap_of_isPretransitive [Group G] [MulAction G α] [Finite α] (S : Set G)
+theorem surjective_of_isSwap_of_isPretransitive [Finite α] (S : Set G)
     (hS1 : ∀ σ ∈ S, Perm.IsSwap (MulAction.toPermHom G α σ)) (hS2 : Subgroup.closure S = ⊤)
     [h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α) := by
   rw [← MonoidHom.range_top_iff_surjective]

Mathlib/GroupTheory/PushoutI.lean

@@ -435,8 +435,7 @@ theorem summand_smul_def' {i : ι} (g : G i) (w : NormalWord d) :
       { equivPair i w with
         head := g * (equivPair i w).head } := rfl
 
-noncomputable instance mulAction [DecidableEq ι] [∀ i, DecidableEq (G i)] :
-    MulAction (PushoutI φ) (NormalWord d) :=
+noncomputable instance mulAction : MulAction (PushoutI φ) (NormalWord d) :=
   MulAction.ofEndHom <|
     lift
       (fun i => MulAction.toEndHom)