chore: bump to nightly-2023-04-11 (#3139)

Mathlib/Algebra/AddTorsor.lean

@@ -285,12 +285,9 @@ end comm
 
 namespace Prod
 
-variable {G : Type _} {P : Type _} {G' : Type _} {P' : Type _} [AddGroup G] [AddGroup G']
-  [AddTorsor G P] [AddTorsor G' P']
+variable {G : Type _} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
 
--- Porting note: the `{_ : ...}` instance terms make this instance not dangerous
-instance {G : Type _} {P : Type _} {G' : Type _} {P' : Type _} {_ : AddGroup G} {_ : AddGroup G'}
-    [AddTorsor G P] [AddTorsor G' P'] : AddTorsor (G × G') (P × P') where
+instance : AddTorsor (G × G') (P × P') where
   vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)
   zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
   add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)

Mathlib/Algebra/Algebra/Equiv.lean

@@ -56,10 +56,9 @@ class AlgEquivClass (F : Type _) (R A B : outParam (Type _)) [CommSemiring R] [S
 
 namespace AlgEquivClass
 
--- Porting note: Replaced instances [...] with {_ : ...} below to make them not dangerous
 -- See note [lower instance priority]
-instance (priority := 100) toAlgHomClass (F R A B : Type _) {_ : CommSemiring R} {_ : Semiring A}
-    {_ : Semiring B} {_ : Algebra R A} {_ : Algebra R B} [h : AlgEquivClass F R A B] :
+instance (priority := 100) toAlgHomClass (F R A B : Type _) [CommSemiring R] [Semiring A]
+    [Semiring B] [Algebra R A] [Algebra R B] [h : AlgEquivClass F R A B] :
     AlgHomClass F R A B :=
   { h with
     coe := (⇑)
@@ -68,8 +67,8 @@ instance (priority := 100) toAlgHomClass (F R A B : Type _) {_ : CommSemiring R}
     map_one := map_one }
 #align alg_equiv_class.to_alg_hom_class AlgEquivClass.toAlgHomClass
 
-instance (priority := 100) toLinearEquivClass (F R A B : Type _) {_ : CommSemiring R}
-    {_ : Semiring A} {_ : Semiring B} {_ : Algebra R A} {_ : Algebra R B}
+instance (priority := 100) toLinearEquivClass (F R A B : Type _) [CommSemiring R]
+    [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
     [h : AlgEquivClass F R A B] : LinearEquivClass F R A B :=
   { h with map_smulₛₗ := fun f => map_smulₛₗ f }
 #align alg_equiv_class.to_linear_equiv_class AlgEquivClass.toLinearEquivClass

Mathlib/Algebra/Algebra/Hom.lean

@@ -65,11 +65,8 @@ namespace AlgHomClass
 variable {R : Type _} {A : Type _} {B : Type _} [CommSemiring R] [Semiring A] [Semiring B]
   [Algebra R A] [Algebra R B]
 
--- Porting note: marked `{}` rather than `[]` to prevent dangerous instances
 -- see Note [lower instance priority]
-instance (priority := 100) linearMapClass {_ : CommSemiring R} {_ : Semiring A} {_ : Semiring B}
-    {_ : Algebra R A} {_ : Algebra R B} {F : Type _} [AlgHomClass F R A B] :
-    LinearMapClass F R A B :=
+instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass F R A B :=
   { ‹AlgHomClass F R A B› with
     map_smulₛₗ := fun f r x => by
       simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply] }

Mathlib/Algebra/EuclideanDomain/Basic.lean

@@ -57,8 +57,7 @@ theorem mod_eq_zero {a b : R} : a % b = 0 ↔ b ∣ a :=
     rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
     haveI := Classical.dec
     by_cases b0 : b = 0
-     --Porting note: `simp` doesn't prove `True` here for some reason
-    · simp only [b0, zero_mul] ; trivial
+    · simp only [b0, zero_mul]
     · rw [mul_div_cancel_left _ b0]⟩
 #align euclidean_domain.mod_eq_zero EuclideanDomain.mod_eq_zero
 

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -117,14 +117,14 @@ variable (F)
 
 -- See note [lower instance priority]
 @[to_additive]
-instance (priority := 100) (F : Type _) {M N : Type _}
-    {_ : Mul M} {_ : Mul N} [h : MulEquivClass F M N] : MulHomClass F M N :=
+instance (priority := 100) (F : Type _)
+    [Mul M] [Mul N] [h : MulEquivClass F M N] : MulHomClass F M N :=
   { h with coe := h.coe, coe_injective' := FunLike.coe_injective' }
 
 -- See note [lower instance priority]
 @[to_additive]
-instance (priority := 100) {_ : MulOneClass M} {_ : MulOneClass N} [MulEquivClass F M N] :
-  MonoidHomClass F M N :=
+instance (priority := 100) [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
+    MonoidHomClass F M N :=
   { MulEquivClass.instMulHomClass F with
     coe := fun _ => _,
     map_one := fun e =>
@@ -138,7 +138,7 @@ instance (priority := 100) {_ : MulOneClass M} {_ : MulOneClass N} [MulEquivClas
 
 -- See note [lower instance priority]
 instance (priority := 100) toMonoidWithZeroHomClass
-  {α β : Type _} {_ : MulZeroOneClass α} {_ : MulZeroOneClass β} [MulEquivClass F α β] :
+    [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
   MonoidWithZeroHomClass F α β :=
   { MulEquivClass.instMonoidHomClass _ with
     map_zero := fun e =>

Mathlib/Algebra/Hom/Group.lean

@@ -544,7 +544,7 @@ attribute [coe] AddMonoidHom.toZeroHom
 
 /-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
 @[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
-instance MonoidHom.coeToOneHom {_ : MulOneClass M} {_ : MulOneClass N} :
+instance MonoidHom.coeToOneHom [MulOneClass M] [MulOneClass N] :
   Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩
 #align monoid_hom.has_coe_to_one_hom MonoidHom.coeToOneHom
 #align add_monoid_hom.has_coe_to_zero_hom AddMonoidHom.coeToZeroHom
@@ -554,22 +554,22 @@ attribute [coe] AddMonoidHom.toAddHom
 
 /-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
 @[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
-instance MonoidHom.coeToMulHom {_ : MulOneClass M} {_ : MulOneClass N} :
+instance MonoidHom.coeToMulHom [MulOneClass M] [MulOneClass N] :
   Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩
 #align monoid_hom.has_coe_to_mul_hom MonoidHom.coeToMulHom
 #align add_monoid_hom.has_coe_to_add_hom AddMonoidHom.coeToAddHom
 
 attribute [coe] MonoidWithZeroHom.toMonoidHom
 
 /-- `MonoidWithZeroHom` down-cast to a `MonoidHom`, forgetting the 0-preserving property. -/
-instance MonoidWithZeroHom.coeToMonoidHom {_ : MulZeroOneClass M} {_ : MulZeroOneClass N} :
+instance MonoidWithZeroHom.coeToMonoidHom [MulZeroOneClass M] [MulZeroOneClass N] :
   Coe (M →*₀ N) (M →* N) := ⟨MonoidWithZeroHom.toMonoidHom⟩
 #align monoid_with_zero_hom.has_coe_to_monoid_hom MonoidWithZeroHom.coeToMonoidHom
 
 attribute [coe] MonoidWithZeroHom.toZeroHom
 
 /-- `MonoidWithZeroHom` down-cast to a `ZeroHom`, forgetting the monoidal property. -/
-instance MonoidWithZeroHom.coeToZeroHom {_ : MulZeroOneClass M} {_ : MulZeroOneClass N} :
+instance MonoidWithZeroHom.coeToZeroHom [MulZeroOneClass M] [MulZeroOneClass N] :
   Coe (M →*₀ N) (ZeroHom M N) := ⟨MonoidWithZeroHom.toZeroHom⟩
 #align monoid_with_zero_hom.has_coe_to_zero_hom MonoidWithZeroHom.coeToZeroHom
 
@@ -804,7 +804,7 @@ equalities. -/
 @[to_additive
   "Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
-protected def OneHom.copy {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
+protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) :
   OneHom M N where
   toFun := f'
   map_one' := h.symm ▸ f.map_one'
@@ -830,7 +830,7 @@ equalities. -/
 @[to_additive
   "Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
-protected def MulHom.copy {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
+protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
   M →ₙ* N where
   toFun := f'
   map_mul' := h.symm ▸ f.map_mul'
@@ -856,7 +856,7 @@ definitional equalities. -/
 @[to_additive
   "Copy of an `AddMonoidHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
-protected def MonoidHom.copy {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
+protected def MonoidHom.copy [MulOneClass M] [MulOneClass N] (f : M →* N) (f' : M → N)
   (h : f' = f) : M →* N :=
   { f.toOneHom.copy f' h, f.toMulHom.copy f' h with }
 #align monoid_hom.copy MonoidHom.copy
@@ -878,7 +878,7 @@ theorem MonoidHom.copy_eq {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N)
 
 /-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
-protected def MonoidWithZeroHom.copy {_ : MulZeroOneClass M} {_ : MulZeroOneClass N} (f : M →*₀ N)
+protected def MonoidWithZeroHom.copy [MulZeroOneClass M] [MulZeroOneClass N] (f : M →*₀ N)
   (f' : M → N) (h : f' = f) : M →* N :=
   { f.toZeroHom.copy f' h, f.toMonoidHom.copy f' h with }
 #align monoid_with_zero_hom.copy MonoidWithZeroHom.copy
@@ -940,7 +940,7 @@ add_decl_doc AddMonoidHom.map_add
 
 namespace MonoidHom
 
-variable {_ : MulOneClass M} {_ : MulOneClass N} [MonoidHomClass F M N]
+variable [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N]
 
 /-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a right inverse,
 then `f x` has a right inverse too. For elements invertible on both sides see `IsUnit.map`. -/
@@ -1457,7 +1457,7 @@ additive morphism sending `x` to `f x + g x`. -/
 add_decl_doc AddHom.instAddAddHomToAddToAddSemigroup
 
 @[to_additive (attr := simp)]
-theorem mul_apply {M N} {_ : Mul M} {_ : CommSemigroup N} (f g : M →ₙ* N) (x : M) :
+theorem mul_apply {M N} [Mul M] [CommSemigroup N] (f g : M →ₙ* N) (x : M) :
   (f * g) x = f x * g x := rfl
 #align mul_hom.mul_apply MulHom.mul_apply
 #align add_hom.add_apply AddHom.add_apply
@@ -1485,7 +1485,7 @@ variable [Group G] [CommGroup H]
 /-- Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism
 sending `x` to `f x * g x`. -/
 @[to_additive]
-instance mul {M N} {_ : MulOneClass M} [CommMonoid N] : Mul (M →* N) :=
+instance mul {M N} [MulOneClass M] [CommMonoid N] : Mul (M →* N) :=
   ⟨fun f g =>
     { toFun := fun m => f m * g m,
       map_one' := show f 1 * g 1 = 1 by simp,
@@ -1499,7 +1499,7 @@ instance mul {M N} {_ : MulOneClass M} [CommMonoid N] : Mul (M →* N) :=
 add_decl_doc AddMonoidHom.add
 
 @[to_additive (attr := simp)]
-theorem mul_apply {M N} {_ : MulOneClass M} {_ : CommMonoid N} (f g : M →* N) (x : M) :
+theorem mul_apply {M N} [MulOneClass M] [CommMonoid N] (f g : M →* N) (x : M) :
   (f * g) x = f x * g x := rfl
 #align monoid_hom.mul_apply MonoidHom.mul_apply
 #align add_monoid_hom.add_apply AddMonoidHom.add_apply
@@ -1652,21 +1652,21 @@ homomorphism sending `x` to `-(f x)`. -/
 add_decl_doc AddMonoidHom.instNegAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup
 
 @[to_additive (attr := simp)]
-theorem inv_apply {M G} {_ : MulOneClass M} {_ : CommGroup G} (f : M →* G) (x : M) :
+theorem inv_apply {M G} [MulOneClass M] [CommGroup G] (f : M →* G) (x : M) :
   f⁻¹ x = (f x)⁻¹ := rfl
 #align monoid_hom.inv_apply MonoidHom.inv_apply
 #align add_monoid_hom.neg_apply AddMonoidHom.neg_apply
 
 @[to_additive (attr := simp)]
-theorem inv_comp {M N A} {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommGroup A}
+theorem inv_comp {M N A} [MulOneClass M] [MulOneClass N] [CommGroup A]
   (φ : N →* A) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹ := by
   ext
   simp only [Function.comp_apply, inv_apply, coe_comp]
 #align monoid_hom.inv_comp MonoidHom.inv_comp
 #align add_monoid_hom.neg_comp AddMonoidHom.neg_comp
 
 @[to_additive (attr := simp)]
-theorem comp_inv {M A B} {_ : MulOneClass M} {_ : CommGroup A} {_ : CommGroup B}
+theorem comp_inv {M A B} [MulOneClass M] [CommGroup A] [CommGroup B]
   (φ : A →* B) (ψ : M →* A) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹ := by
   ext
   simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]
@@ -1685,7 +1685,7 @@ is the homomorphism sending `x` to `(f x) - (g x)`. -/
 add_decl_doc AddMonoidHom.instSubAddMonoidHomToAddZeroClassToAddMonoidToSubNegAddMonoidToAddGroup
 
 @[to_additive (attr := simp)]
-theorem div_apply {M G} {_ : MulOneClass M} {_ : CommGroup G} (f g : M →* G) (x : M) :
+theorem div_apply {M G} [MulOneClass M] [CommGroup G] (f g : M →* G) (x : M) :
   (f / g) x = f x / g x := rfl
 #align monoid_hom.div_apply MonoidHom.div_apply
 #align add_monoid_hom.sub_apply AddMonoidHom.sub_apply
@@ -1694,7 +1694,7 @@ end MonoidHom
 
 /-- Given two monoid with zero morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid
 with zero morphism sending `x` to `f x * g x`. -/
-instance {M N} {_ : MulZeroOneClass M} [CommMonoidWithZero N] : Mul (M →*₀ N) :=
+instance [MulZeroOneClass M] [CommMonoidWithZero N] : Mul (M →*₀ N) :=
   ⟨fun f g => { (f * g : M →* N) with
     toFun := fun a => f a * g a,
     map_zero' := by dsimp only []; rw [map_zero, zero_mul] }⟩

Mathlib/Algebra/Hom/NonUnitalAlg.lean

@@ -78,17 +78,17 @@ class NonUnitalAlgHomClass (F : Type _) (R : outParam (Type _)) (A : outParam (T
 
 namespace NonUnitalAlgHomClass
 
--- Porting note: Made following instance non-dangerous through [...] -> {_ : ...} replacement
+-- Porting note: Made following instance non-dangerous through [...] -> [...] replacement
 -- See note [lower instance priority]
 instance (priority := 100) toNonUnitalRingHomClass {F R A B : Type _}
-    {_ : Monoid R} {_ : NonUnitalNonAssocSemiring A} {_ : DistribMulAction R A}
-    {_ : NonUnitalNonAssocSemiring B} {_ : DistribMulAction R B}
+    [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
+    [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
     [NonUnitalAlgHomClass F R A B] : NonUnitalRingHomClass F A B :=
   { ‹NonUnitalAlgHomClass F R A B› with coe := (⇑) }
 #align non_unital_alg_hom_class.non_unital_alg_hom_class.to_non_unital_ring_hom_class NonUnitalAlgHomClass.toNonUnitalRingHomClass
 
-variable {_ : Semiring R} {_ : NonUnitalNonAssocSemiring A} {_ : Module R A}
-  {_ : NonUnitalNonAssocSemiring B} {_ : Module R B}
+variable [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A]
+  [NonUnitalNonAssocSemiring B] [Module R B]
 
 -- see Note [lower instance priority]
 instance (priority := 100) {F : Type _} [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B :=
@@ -414,11 +414,11 @@ end NonUnitalAlgHom
 
 namespace AlgHom
 
-variable {R A B} {_ : CommSemiring R} {_ : Semiring A} {_ : Semiring B} {_ : Algebra R A}
-  {_ : Algebra R B}
+variable {R A B} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
+  [Algebra R B]
 
 -- see Note [lower instance priority]
-instance (priority := 100) {F : Type _} [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B :=
+instance (priority := 100) [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B :=
   { ‹AlgHomClass F R A B› with map_smul := map_smul }
 
 /-- A unital morphism of algebras is a `NonUnitalAlgHom`. -/

Mathlib/Algebra/Hom/Ring.lean

@@ -106,13 +106,7 @@ namespace NonUnitalRingHom
 
 section coe
 
-/-!
-Throughout this section, some `Semiring` arguments are specified with `{}` instead of `[]`.
-See note [implicit instance arguments].
--/
-
-
-variable {_ : NonUnitalNonAssocSemiring α} {_ : NonUnitalNonAssocSemiring β}
+variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β]
 
 instance : NonUnitalRingHomClass (α →ₙ+* β) α β where
   coe f := f.toFun
@@ -179,7 +173,7 @@ end coe
 
 section
 
-variable {_ : NonUnitalNonAssocSemiring α} {_ : NonUnitalNonAssocSemiring β}
+variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β]
 variable (f : α →ₙ+* β) {x y : α}
 
 @[ext]
@@ -246,7 +240,7 @@ theorem coe_mulHom_id : (NonUnitalRingHom.id α : α →ₙ* α) = MulHom.id α
   rfl
 #align non_unital_ring_hom.coe_mul_hom_id NonUnitalRingHom.coe_mulHom_id
 
-variable {_ : NonUnitalNonAssocSemiring γ}
+variable [NonUnitalNonAssocSemiring γ]
 
 /-- Composition of non-unital ring homomorphisms is a non-unital ring homomorphism. -/
 def comp (g : β →ₙ+* γ) (f : α →ₙ+* β) : α →ₙ+* γ :=

Mathlib/Algebra/Module/Equiv.lean

@@ -122,7 +122,6 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂]
 
 variable [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R}
 
-@[infer_tc_goals_rl, nolint dangerousInstance]
 instance (priority := 100) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
   [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂ :=
   { s with

Mathlib/Algebra/Module/LinearMap.lean

@@ -155,14 +155,13 @@ abbrev LinearMapClass (F : Type _) (R M M₂ : outParam (Type _)) [Semiring R] [
 namespace SemilinearMapClass
 
 variable (F : Type _)
-variable {_ : Semiring R} {_ : Semiring S}
-variable {_ : AddCommMonoid M} {_ : AddCommMonoid M₁} {_ : AddCommMonoid M₂} {_ : AddCommMonoid M₃}
-variable {_ : AddCommMonoid N₁} {_ : AddCommMonoid N₂} {_ : AddCommMonoid N₃}
-variable {_ : Module R M} {_ : Module R M₂} {_ : Module S M₃}
+variable [Semiring R] [Semiring S]
+variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
+variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃]
+variable [Module R M] [Module R M₂] [Module S M₃]
 variable {σ : R →+* S}
 
 -- Porting note: the `dangerousInstance` linter has become smarter about `outParam`s
--- @[nolint dangerousInstance] -- `σ` is an `outParam` so it's not dangerous
 instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] :
     AddMonoidHomClass F M M₃ :=
   { SemilinearMapClass.toAddHomClass with
@@ -172,10 +171,6 @@ instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] :
         rw [← zero_smul R (0 : M), map_smulₛₗ]
         simp }
 
--- The `Semiring` should be an instance parameter but depends on outParams.
--- If Lean 4 gets better support for instance params depending on outParams,
--- we should be able to remove this nolint.
-@[nolint dangerousInstance]
 instance (priority := 100) distribMulActionHomClass [LinearMapClass F R M M₂] :
     DistribMulActionHomClass F R M M₂ :=
   { SemilinearMapClass.addMonoidHomClass F with

Mathlib/Algebra/Module/Pi.lean

@@ -101,7 +101,7 @@ instance module' {g : I → Type _} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddC
     rw [zero_smul]
 #align pi.module' Pi.module'
 
-instance noZeroSMulDivisors (α) {_ : Semiring α} {_ : ∀ i, AddCommMonoid <| f i}
+instance noZeroSMulDivisors (α) [Semiring α] [∀ i, AddCommMonoid <| f i]
     [∀ i, Module α <| f i] [∀ i, NoZeroSMulDivisors α <| f i] :
     NoZeroSMulDivisors α (∀ i : I, f i) :=
   ⟨fun {_ _} h =>
@@ -110,7 +110,7 @@ instance noZeroSMulDivisors (α) {_ : Semiring α} {_ : ∀ i, AddCommMonoid <|
 
 /-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
 synthesize this instance by itself elsewhere in the library. -/
-instance _root_.Function.noZeroSMulDivisors {ι α β : Type _} {_ : Semiring α} {_ : AddCommMonoid β}
+instance _root_.Function.noZeroSMulDivisors {ι α β : Type _} [Semiring α] [AddCommMonoid β]
     [Module α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
   Pi.noZeroSMulDivisors _
 #align function.no_zero_smul_divisors Function.noZeroSMulDivisors

Mathlib/Algebra/Module/Prod.lean

@@ -36,7 +36,7 @@ instance mulActionWithZero [MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZe
     zero_smul := fun _ => Prod.ext (zero_smul _ _) (zero_smul _ _) }
 #align prod.mul_action_with_zero Prod.mulActionWithZero
 
-instance module {_ : Semiring R} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
+instance module [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
     Module R (M × N) :=
   { Prod.distribMulAction with
     add_smul := fun _ _ _ => mk.inj_iff.mpr ⟨add_smul _ _ _, add_smul _ _ _⟩