case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ x✝ ∈ I • Submodule.span R (Set.range v)
ι : Type u_3
M : Type u_1
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) = ⊤
⊢ LinearMap.range (finsuppTotal ι M I v) = I • Submodule.span R (Set.range v)
ext
case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ ∃ a x, (Finsupp.sum a fun i c => c • v i) = x✝
case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ x✝ ∈ I • Submodule.span R (Set.range v)
rw [Submodule.mem_ideal_smul_span_iff_exists_sum]
case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ (∃ a x, (Finsupp.sum a fun i c => c • v i) = x✝) → x✝ ∈ LinearMap.range (finsuppTotal ι M I v)
case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ ∃ a x, (Finsupp.sum a fun i c => c • v i) = x✝
refine' ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, _⟩
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun i c => c • v i) ∈ LinearMap.range (finsuppTotal ι M I v)
case h
ι : Type u_3
M : Type u_1
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) = ⊤
x✝ : M
⊢ (∃ a x, (Finsupp.sum a fun i c => c • v i) = x✝) → x✝ ∈ LinearMap.range (finsuppTotal ι M I v)
rintro ⟨a, ha, rfl⟩
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ↑(finsuppTotal ι M I v)
      (Finsupp.mapRange (fun r => if h : r ∈ I then { val := r, property := h } else 0)
        (_ : (if h : 0 ∈ I then { val := 0, property := h } else 0) = 0) a) =
    Finsupp.sum a fun i c => c • v i
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun i c => c • v i) ∈ LinearMap.range (finsuppTotal ι M I v)
refine' ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0) (by simp), _⟩
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun a b => ↑(if h : b ∈ I then { val := b, property := h } else 0) • v a) =
    Finsupp.sum a fun i c => c • v i

case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ↑(finsuppTotal ι M I v)
      (Finsupp.mapRange (fun r => if h : r ∈ I then { val := r, property := h } else 0)
        (_ : (if h : 0 ∈ I then { val := 0, property := h } else 0) = 0) a) =
    Finsupp.sum a fun i c => c • v i
rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
no goals
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (fun r => if h : r ∈ I then { val := r, property := h } else 0) 0 = 0
simp
case h.intro.intro.h
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∀ (x : ι), x ∈ a.support → ↑(if h : ↑a x ∈ I then { val := ↑a x, property := h } else 0) • v x = ↑a x • v x
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun a b => ↑(if h : b ∈ I then { val := b, property := h } else 0) • v a) =
    Finsupp.sum a fun i c => c • v i
apply Finsupp.sum_congr
case h.intro.intro.h
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : ↑a i ∈ I then { val := ↑a i, property := h } else 0) • v i = ↑a i • v i
case h.intro.intro.h
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∀ (x : ι), x ∈ a.support → ↑(if h : ↑a x ∈ I then { val := ↑a x, property := h } else 0) • v x = ↑a x • v x
intro i _
no goals
case h.intro.intro.h
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : ↑a i ∈ I then { val := ↑a i, property := h } else 0) • v i = ↑a i • v i
rw [dif_pos (ha i)]
no goals
case h.intro.intro
ι : Type u_3
M : Type u_1
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) = ⊤
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0
exact fun _ => zero_smul _ _