diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
index c27bc8418750f..806b3702c7c54 100644
--- a/src/algebra/direct_limit.lean
+++ b/src/algebra/direct_limit.lean
@@ -175,7 +175,7 @@ span_induction ((quotient.mk_eq_zero _).1 H)
           to_module_totalize_of_le hik hi,
           to_module_totalize_of_le hjk hj]⟩)
   (λ a x ⟨i, hi, hxi⟩,
-    ⟨i, λ k hk, hi k (dfinsupp.support_smul hk),
+    ⟨i, λ k hk, hi k (direct_sum.support_smul _ _ hk),
       by simp [linear_map.map_smul, hxi]⟩)
 
 /-- A component that corresponds to zero in the direct limit is already zero in some
diff --git a/src/algebra/direct_sum.lean b/src/algebra/direct_sum.lean
index 017e50a83ebd2..0c0ff65a01271 100644
--- a/src/algebra/direct_sum.lean
+++ b/src/algebra/direct_sum.lean
@@ -39,6 +39,13 @@ namespace direct_sum
 
 variables {ι}
 
+@[simp] lemma zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 := rfl
+
+variables {β}
+@[simp] lemma add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i :=
+dfinsupp.add_apply _ _ _
+
+variables (β)
 include dec_ι
 
 /-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean
index 75ff955dc71d8..3facb8bd7805c 100644
--- a/src/algebra/lie/basic.lean
+++ b/src/algebra/lie/basic.lean
@@ -306,7 +306,8 @@ instance : lie_ring (⨁ i, L i) :=
   add_lie  := λ x y z, by { ext, simp only [zip_with_apply, add_apply, add_lie], },
   lie_add  := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_add], },
   lie_self := λ x, by { ext, simp only [zip_with_apply, add_apply, lie_self, zero_apply], },
-  jacobi   := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_ring.jacobi, zero_apply], },
+  jacobi   := λ x y z, by { ext, simp only [
+    zip_with_apply, add_apply, lie_ring.jacobi, zero_apply], },
   ..(infer_instance : add_comm_group _) }
 
 @[simp] lemma bracket_apply {x y : (⨁ i, L i)} {i : ι} :
@@ -314,7 +315,8 @@ instance : lie_ring (⨁ i, L i) :=
 
 /-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/
 instance : lie_algebra R (⨁ i, L i) :=
-{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, smul_apply, bracket_apply, lie_smul], },
+{ lie_smul := λ c x y, by { ext, simp only [
+    zip_with_apply, direct_sum.smul_apply, bracket_apply, lie_smul] },
   ..(infer_instance : module R _) }
 
 end direct_sum
@@ -341,8 +343,8 @@ def of_associative_algebra_hom {R : Type u} {A : Type v} {B : Type w}
      by simp only [lie_ring.of_associative_ring_bracket, alg_hom.map_sub, alg_hom.map_mul],
   ..f.to_linear_map, }
 
-@[simp] lemma of_associative_algebra_hom_id {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] :
-  of_associative_algebra_hom (alg_hom.id R A) = 1 := rfl
+@[simp] lemma of_associative_algebra_hom_id {R : Type u} {A : Type v}
+  [comm_ring R] [ring A] [algebra R A] : of_associative_algebra_hom (alg_hom.id R A) = 1 := rfl
 
 @[simp] lemma of_associative_algebra_hom_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁}
   [comm_ring R] [ring A] [ring B] [ring C] [algebra R A] [algebra R B] [algebra R C]
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index cfaabf9e36341..7abe0156622b9 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -64,8 +64,7 @@ instance : inhabited (Π₀ i, β i) := ⟨0⟩
 
 @[simp] lemma zero_apply (i : ι) : (0 : Π₀ i, β i) i = 0 := rfl
 
-@[ext]
-lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g :=
+@[ext] lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g :=
 quotient.induction_on₂ f g (λ _ _ H, quotient.sound H) H
 
 /-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is
@@ -147,21 +146,22 @@ instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) :=
 
 /-- Dependent functions with finite support inherit a semiring action from an action on each
 coordinate. -/
-def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] :
+def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] :
   has_scalar γ (Π₀ i, β i) :=
 ⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩
 local attribute [instance] to_has_scalar
 
-@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)]
+@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)]
   [Π i, semimodule γ (β i)] (b : γ) (v : Π₀ i, β i) (i : ι) :
   (b • v) i = b • (v i) :=
 map_range_apply _ _ v i
 
 /-- Dependent functions with finite support inherit a semimodule structure from such a structure on
 each coordinate. -/
-def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] :
+def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] :
   semimodule γ (Π₀ i, β i) :=
-semimodule.of_core {
+{ smul_zero := λ c, ext $ λ i, by simp only [smul_apply, smul_zero, zero_apply],
+  zero_smul := λ c, ext $ λ i, by simp only [smul_apply, zero_smul, zero_apply],
   smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add],
   add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul],
   one_smul := λ x, ext $ λ i, by simp only [smul_apply, one_smul],
@@ -431,7 +431,7 @@ instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β
 
 section
 local attribute [instance] to_semimodule
-variables (γ : Type w) [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)]
+variables (γ : Type w) [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)]
 include γ
 
 @[simp] lemma mk_smul {s : finset ι} {c : γ} (x : Π i : (↑s : set ι), β i.1) :
@@ -608,9 +608,9 @@ by ext i; simp
 
 local attribute [instance] dfinsupp.to_semimodule
 
-lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
-  [Π (i : ι) (x : β i), decidable (x ≠ 0)]
-  {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support :=
+lemma support_smul {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)]
+  [Π ( i : ι) (x : β i), decidable (x ≠ 0)]
+  (b : γ) (v : Π₀ i, β i) : (b • v).support ⊆ v.support :=
 support_map_range
 
 instance [Π i, has_zero (β i)] [Π i, decidable_eq (β i)] : decidable_eq (Π₀ i, β i) :=
diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean
index fb5ccf8626ca4..ee8d8f0eb598d 100644
--- a/src/linear_algebra/direct_sum_module.lean
+++ b/src/linear_algebra/direct_sum_module.lean
@@ -36,7 +36,10 @@ open_locale direct_sum
 
 variables {R ι M}
 
-instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
+instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ _ _
+
+@[simp] lemma smul_apply (b : R) (v : ⨁ i, M i) (i : ι) :
+  (b • v) i = b • (v i) := dfinsupp.smul_apply _ _ _
 
 include dec_ι
 
@@ -61,10 +64,14 @@ theorem mk_smul (s : finset ι) (c : R) (x) : mk M s (c • x) = c • mk M s x
 theorem of_smul (i : ι) (c : R) (x) : of M i (c • x) = c • of M i x :=
 (lof R ι M i).map_smul c x
 
+variables {R}
+lemma support_smul [Π (i : ι) (x : M i), decidable (x ≠ 0)]
+  (c : R) (v : ⨁ i, M i) : (c • v).support ⊆ v.support := dfinsupp.support_smul _ _
+
 variables {N : Type u₁} [add_comm_group N] [semimodule R N]
 variables (φ : Π i, M i →ₗ[R] N)
 
-variables (ι N φ)
+variables (R ι N φ)
 /-- The linear map constructed using the universal property of the coproduct. -/
 def to_module : (⨁ i, M i) →ₗ[R] N :=
 { to_fun := to_group (λ i, (φ i).to_add_monoid_hom),