diff --git a/Mathlib/Algebra/DirectSum/Module.lean b/Mathlib/Algebra/DirectSum/Module.lean
index 4f6e05790646a2..6b5cc38f8d4b93 100644
--- a/Mathlib/Algebra/DirectSum/Module.lean
+++ b/Mathlib/Algebra/DirectSum/Module.lean
@@ -40,8 +40,6 @@ variable {R : Type u} [Semiring R]
 
 variable {ι : Type v} [dec_ι : DecidableEq ι]
 
-include R
-
 variable {M : ι → Type w} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
 
 instance : Module R (⨁ i, M i) :=
@@ -49,7 +47,7 @@ instance : Module R (⨁ i, M i) :=
 
 instance {S : Type _} [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] :
     SMulCommClass R S (⨁ i, M i) :=
-  Dfinsupp.sMulCommClass
+  Dfinsupp.smulCommClass
 
 instance {S : Type _} [Semiring S] [SMul R S] [∀ i, Module S (M i)] [∀ i, IsScalarTower R S (M i)] :
     IsScalarTower R S (⨁ i, M i) :=
@@ -62,8 +60,6 @@ theorem smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : (b • v) i = b • v i :
   Dfinsupp.smul_apply _ _ _
 #align direct_sum.smul_apply DirectSum.smul_apply
 
-include dec_ι
-
 variable (R ι M)
 
 /-- Create the direct sum given a family `M` of `R` modules indexed over `ι`. -/
@@ -107,11 +103,11 @@ variable {N : Type u₁} [AddCommMonoid N] [Module R N]
 
 variable (φ : ∀ i, M i →ₗ[R] N)
 
-variable (R ι N φ)
+variable (R ι N)
 
 /-- The linear map constructed using the universal property of the coproduct. -/
 def toModule : (⨁ i, M i) →ₗ[R] N :=
-  Dfinsupp.lsum ℕ φ
+  FunLike.coe (Dfinsupp.lsum ℕ) φ
 #align direct_sum.to_module DirectSum.toModule
 
 /-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor
@@ -153,11 +149,9 @@ theorem linearMap_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄
 into a larger subset of the direct summands, as a linear map.
 -/
 def lsetToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, M i) →ₗ[R] ⨁ i : T, M i :=
-  toModule R _ _ fun i => lof R T (fun i : Subtype T => M i) ⟨i, H i.Prop⟩
+  toModule R _ _ fun i => lof R T (fun i : Subtype T => M i) ⟨i, H i.prop⟩
 #align direct_sum.lset_to_set DirectSum.lsetToSet
 
-omit dec_ι
-
 variable (ι M)
 
 /-- Given `fintype α`, `linear_equiv_fun_on_fintype R` is the natural `R`-linear equivalence
@@ -165,13 +159,14 @@ between `⨁ i, M i` and `Π i, M i`. -/
 @[simps apply]
 def linearEquivFunOnFintype [Fintype ι] : (⨁ i, M i) ≃ₗ[R] ∀ i, M i :=
   { Dfinsupp.equivFunOnFintype with
-    toFun := coeFn
+    toFun := (↑)
     map_add' := fun f g => by
       ext
       simp only [add_apply, Pi.add_apply]
     map_smul' := fun c f => by
       ext
-      simp only [Dfinsupp.coe_smul, RingHom.id_apply] }
+      simp only [Dfinsupp.coe_smul, RingHom.id_apply]
+      rfl }
 #align direct_sum.linear_equiv_fun_on_fintype DirectSum.linearEquivFunOnFintype
 
 variable {ι M}
@@ -457,4 +452,3 @@ end Ring
 end Submodule
 
 end DirectSum
-
diff --git a/Mathlib/Data/Dfinsupp/Basic.lean b/Mathlib/Data/Dfinsupp/Basic.lean
index 12a4e4365aecb6..9daa98dd325d81 100644
--- a/Mathlib/Data/Dfinsupp/Basic.lean
+++ b/Mathlib/Data/Dfinsupp/Basic.lean
@@ -360,16 +360,17 @@ theorem coe_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction
   rfl
 #align dfinsupp.coe_smul Dfinsupp.coe_smul
 
-instance {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
-    [∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] : SMulCommClass γ δ (Π₀ i, β i)
+instance smulCommClass {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
+    [∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] :
+    SMulCommClass γ δ (Π₀ i, β i)
     where smul_comm r s m := ext fun i => by simp only [smul_apply, smul_comm r s (m i)]
 
-instance {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
-    [∀ i, DistribMulAction δ (β i)] [SMul γ δ] [∀ i, IsScalarTower γ δ (β i)] :
-    IsScalarTower γ δ (Π₀ i, β i)
+instance isScalarTower {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
+    [∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [SMul γ δ]
+    [∀ i, IsScalarTower γ δ (β i)] : IsScalarTower γ δ (Π₀ i, β i)
     where smul_assoc r s m := ext fun i => by simp only [smul_apply, smul_assoc r s (m i)]
 
-instance [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
+instance isCentralScalar [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
     [∀ i, DistribMulAction γᵐᵒᵖ (β i)] [∀ i, IsCentralScalar γ (β i)] :
     IsCentralScalar γ (Π₀ i, β i)
     where op_smul_eq_smul r m := ext fun i => by simp only [smul_apply, op_smul_eq_smul r (m i)]