case mp
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x

case mpr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
constructor
case mpr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)

case mp
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
case mp
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x

case mpr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)
swap
case mp.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x : M),
    (x ∈ ⋃ (a : R) (_ : a ∈ I) (b : M) (_ : b ∈ Set.range f), {a • b}) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x

case mp.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = 0

case mp.refine'_3
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) →
      (∃ a x, (Finsupp.sum a fun i c => c • f i) = y) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x + y

case mp.refine'_4
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R) (x : M),
    (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → ∃ a_2 x_1, (Finsupp.sum a_2 fun i c => c • f i) = a • x
case mp
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
refine' fun hx => span_induction (mem_smul_span.mp hx) _ _ _ _
case mpr.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun i c => c • f i) ∈ I • span R (Set.range f)
case mpr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
⊢ (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)
rintro ⟨a, ha, rfl⟩
no goals
case mpr.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum a fun i c => c • f i) ∈ I • span R (Set.range f)
exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _
case mp.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x : M), (∃ i h i_1 h, x = i • i_1) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
case mp.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x : M),
    (x ∈ ⋃ (a : R) (_ : a ∈ I) (b : M) (_ : b ∈ Set.range f), {a • b}) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
simp only [Set.mem_iUnion, Set.mem_range, Set.mem_singleton_iff]
case mp.refine'_1.intro.intro.intro.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = y • f i
case mp.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x : M), (∃ i h i_1 h, x = i • i_1) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x
rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
⊢ ↑(Finsupp.single i y) j ∈ I

case mp.refine'_1.intro.intro.intro.intro.intro.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ (Finsupp.sum (Finsupp.single i y) fun i c => c • f i) = y • f i
case mp.refine'_1.intro.intro.intro.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = y • f i
refine' ⟨Finsupp.single i y, fun j => _, _⟩
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ (fun i y => y • f i) i 0 = 0
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ (Finsupp.sum (Finsupp.single i y) fun i c => c • f i) = y • f i
refine' @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) _
no goals
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ (fun i y => y • f i) i 0 = 0
simp
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finsupp.single i y) j ∈ I
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
⊢ ↑(Finsupp.single i y) j ∈ I
letI := Classical.decEq ι
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (if i = j then y else 0) ∈ I
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finsupp.single i y) j ∈ I
rw [Finsupp.single_apply]
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1.inl
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : i = j
⊢ y ∈ I

case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1.inr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (if i = j then y else 0) ∈ I
split_ifs
no goals
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1.inl
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : i = j
⊢ y ∈ I
assumption
no goals
case mp.refine'_1.intro.intro.intro.intro.intro.refine'_1.inr
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I
exact I.zero_mem
no goals
case mp.refine'_2
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = 0
exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩
case mp.refine'_3.intro.intro.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ↑ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ↑ay i ∈ I
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = (Finsupp.sum ax fun i c => c • f i) + Finsupp.sum ay fun i c => c • f i
case mp.refine'_3
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) →
      (∃ a x, (Finsupp.sum a fun i c => c • f i) = y) → ∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x + y
rintro x y ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩
no goals
case mp.refine'_3.intro.intro.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ↑ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ↑ay i ∈ I
⊢ ∃ a x, (Finsupp.sum a fun i c => c • f i) = (Finsupp.sum ax fun i c => c • f i) + Finsupp.sum ay fun i c => c • f i
refine' ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' _ _⟩ <;> intros <;>
  simp only [zero_smul, add_smul]
case mp.refine'_4.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∃ a_1 x, (Finsupp.sum a_1 fun i c => c • f i) = c • Finsupp.sum a fun i c => c • f i
case mp.refine'_4
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R) (x : M),
    (∃ a x_1, (Finsupp.sum a fun i c => c • f i) = x) → ∃ a_2 x_1, (Finsupp.sum a_2 fun i c => c • f i) = a • x
rintro c x ⟨a, ha, rfl⟩
case mp.refine'_4.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum (c • a) fun i c => c • f i) = c • Finsupp.sum a fun i c => c • f i
case mp.refine'_4.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ ∃ a_1 x, (Finsupp.sum a_1 fun i c => c • f i) = c • Finsupp.sum a fun i c => c • f i
refine' ⟨c • a, fun i => I.mul_mem_left c (ha i), _⟩
no goals
case mp.refine'_4.intro.intro
R : Type u
M : Type v
F : Type ?u.142173
G : Type ?u.142176
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), ↑a i ∈ I
⊢ (Finsupp.sum (c • a) fun i c => c • f i) = c • Finsupp.sum a fun i c => c • f i
rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]