From 072cfc55d54d5c4ee9c28cb42072b6cd04ea5ec0 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 30 Oct 2020 08:20:14 +0000
Subject: [PATCH] chore(data/dfinsupp): Provide dfinsupp with a semimodule
 instance (#4801)

finsupp already has one, it seems pointless to hide the one for dfinsupp behind a def.
---
 src/data/dfinsupp.lean                    | 8 ++------
 src/linear_algebra/direct_sum_module.lean | 2 +-
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index d241b9a4304df..b1cd323e28a53 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -147,10 +147,9 @@ 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_monoid (β i)] [Π i, semimodule γ (β i)] :
+instance {γ : 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_monoid (β i)]
   [Π i, semimodule γ (β i)] (b : γ) (v : Π₀ i, β i) (i : ι) :
@@ -159,7 +158,7 @@ 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_monoid (β i)] [Π i, semimodule γ (β i)] :
+instance {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] :
   semimodule γ (Π₀ i, β i) :=
 { 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],
@@ -431,7 +430,6 @@ instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β
 { map_add := λ _ _, mk_add }
 
 section
-local attribute [instance] to_semimodule
 variables (γ : Type w) [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)]
 include γ
 
@@ -607,8 +605,6 @@ support_zip_with
   support (-f) = support f :=
 by ext i; simp
 
-local attribute [instance] dfinsupp.to_semimodule
-
 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 :=
diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean
index 05ff525db4306..996af06e2542f 100644
--- a/src/linear_algebra/direct_sum_module.lean
+++ b/src/linear_algebra/direct_sum_module.lean
@@ -36,7 +36,7 @@ open_locale direct_sum
 
 variables {R ι M}
 
-instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
+instance : semimodule R (⨁ i, M i) := dfinsupp.semimodule
 
 lemma smul_apply (b : R) (v : ⨁ i, M i) (i : ι) :
   (b • v) i = b • (v i) := dfinsupp.smul_apply _ _ _