-- Mathlib/RingTheory/Ideal/Operations.lean
theorem range_finsuppTotal :
    LinearMap.range (finsuppTotal ι M I v) = I • Submodule.span R (Set.range v)

Proof state:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ x✝ ∈ I • Submodule.span R (Set.range v)

Tactic:
rw [Submodule.mem_ideal_smul_span_iff_exists_sum]

Result:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝

Proof state:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝

Tactic:
refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩

Result:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝) → x✝ ∈ LinearMap.range (finsuppTotal ι M I v)

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
⊢ LinearMap.range (finsuppTotal ι M I v) = I • Submodule.span R (Set.range v)

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ x✝ ∈ I • Submodule.span R (Set.range v)

Proof state:
case h.intro.intro.h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ x ∈ a.support, ↑(if h : a x ∈ I then ⟨a x, h⟩ else 0) • v x = a x • v x

Tactic:
intro i _

Result:
case h.intro.intro.h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : a i ∈ I then ⟨a i, h⟩ else 0) • v i = a i • v i

Proof state:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0

Tactic:
exact fun _ => zero_smul _ _

Result:
no goals

Proof state:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i c => c • v i) ∈ LinearMap.range (finsuppTotal ι M I v)

Tactic:
refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
  (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩

Result:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (finsuppTotal ι M I v) (Finsupp.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a) = a.sum fun i c => c • v i

Proof state:
case h.intro.intro.h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : a i ∈ I then ⟨a i, h⟩ else 0) • v i = a i • v i

Tactic:
rw [dif_pos (ha i)]

Result:
no goals

Proof state:
case h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝) → x✝ ∈ LinearMap.range (finsuppTotal ι M I v)

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i c => c • v i) ∈ LinearMap.range (finsuppTotal ι M I v)

Proof state:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (finsuppTotal ι M I v) (Finsupp.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a) = a.sum fun i c => c • v i

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]

Result:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b => ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c => c • v i

case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (fun r => if h : r ∈ I then ⟨r, h⟩ else 0) 0 = 0

Tactic:
simp only [Submodule.zero_mem, ↓reduceDIte]

Result:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ⟨0, ⋯⟩ = 0

Proof state:
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b => ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c => c • v i

Tactic:
apply Finsupp.sum_congr

Result:
case h.intro.intro.h
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ x ∈ a.support, ↑(if h : a x ∈ I then ⟨a x, h⟩ else 0) • v x = a x • v x