ι : Type u_1
M : Type u_3
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
f : ι →₀ { x // x ∈ I }
⊢ ↑(Finsupp.total ι M R v) (Finsupp.mapRange Subtype.val (_ : ↑(Submodule.subtype I) 0 = 0) f) =
    Finsupp.sum f fun i x => ↑x • v i
ι : Type u_1
M : Type u_3
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
f : ι →₀ { x // x ∈ I }
⊢ ↑(finsuppTotal ι M I v) f = Finsupp.sum f fun i x => ↑x • v i
dsimp [finsuppTotal]
ι : Type u_1
M : Type u_3
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
f : ι →₀ { x // x ∈ I }
⊢ ∀ (a : ι), 0 • v a = 0
ι : Type u_1
M : Type u_3
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
f : ι →₀ { x // x ∈ I }
⊢ ↑(Finsupp.total ι M R v) (Finsupp.mapRange Subtype.val (_ : ↑(Submodule.subtype I) 0 = 0) f) =
    Finsupp.sum f fun i x => ↑x • v i
rw [Finsupp.total_apply, Finsupp.sum_mapRange_index]
no goals
ι : Type u_1
M : Type u_3
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
f : ι →₀ { x // x ∈ I }
⊢ ∀ (a : ι), 0 • v a = 0
exact fun _ => zero_smul _ _