ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
ha : ∃ y, y ∈ Finsupp.supported R R (univ \ {i}) ∧ ↑(Finsupp.total ι M R v) y = a • v i
⊢ a = 0
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ span R (v '' (univ \ {i}))
⊢ a = 0
rw [Finsupp.span_image_eq_map_total, mem_map] at ha
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
⊢ a = 0
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
ha : ∃ y, y ∈ Finsupp.supported R R (univ \ {i}) ∧ ↑(Finsupp.total ι M R v) y = a • v i
⊢ a = 0
rcases ha with ⟨l, hl, e⟩
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
⊢ a = 0
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
⊢ a = 0
rw [sub_eq_zero.1 (linearIndependent_iff.1 hv (l - Finsupp.single i a) (by simp [e]))] at hl
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
hn : ¬a = 0
⊢ False
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
⊢ a = 0
by_contra hn
no goals
case intro.intro
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
hn : ¬a = 0
⊢ False
exact (not_mem_of_mem_diff (hl <| by simp [hn])) (mem_singleton _)
no goals
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
⊢ ↑(Finsupp.total ι M R v) (l - Finsupp.single i a) = 0
simp [e]
no goals
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a✝ b : R
x y : M
hv✝ hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : ↑(Finsupp.total ι M R v) l = a • v i
hn : ¬a = 0
⊢ i ∈ ↑(Finsupp.single i a).support
simp [hn]
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
⊢ ↑l i = ↑0 i
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
⊢ l = 0
ext i
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
⊢ ↑l i = 0
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
⊢ ↑l i = ↑0 i
simp only [Finsupp.zero_apply]
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ False
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
⊢ ↑l i = 0
by_contra hn
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ↑l i • v i ∈ span R (v '' (univ \ {i}))
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ False
refine' hn (H i _ _)
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ Finsupp.single i (↑l i) - l ∈ Finsupp.supported R R (univ \ {i})

case h.refine'_2
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i (↑l i) - l) = ↑l i • v i
case h
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ↑l i • v i ∈ span R (v '' (univ \ {i}))
refine' (Finsupp.mem_span_image_iff_total R).2 ⟨Finsupp.single i (l i) - l, _, _⟩
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ∀ (x : ι), ¬x ∈ univ \ {i} → ↑(Finsupp.single i (↑l i) - l) x = 0
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ Finsupp.single i (↑l i) - l ∈ Finsupp.supported R R (univ \ {i})
rw [Finsupp.mem_supported']
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
j : ι
hj : ¬j ∈ univ \ {i}
⊢ ↑(Finsupp.single i (↑l i) - l) j = 0
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ∀ (x : ι), ¬x ∈ univ \ {i} → ↑(Finsupp.single i (↑l i) - l) x = 0
intro j hj
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
j : ι
hj : ¬j ∈ univ \ {i}
hij : j = i
⊢ ↑(Finsupp.single i (↑l i) - l) j = 0
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
j : ι
hj : ¬j ∈ univ \ {i}
⊢ ↑(Finsupp.single i (↑l i) - l) j = 0
have hij : j = i :=
  Classical.not_not.1 fun hij : j ≠ i =>
    hj ((mem_diff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
no goals
case h.refine'_1
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
j : ι
hj : ¬j ∈ univ \ {i}
hij : j = i
⊢ ↑(Finsupp.single i (↑l i) - l) j = 0
simp [hij]
no goals
case h.refine'_2
ι : Type u'
ι' : Type ?u.472009
R : Type u_1
K : Type ?u.472015
M : Type u_2
M' : Type ?u.472021
M'' : Type ?u.472024
V : Type u
V' : Type ?u.472029
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : ↑(Finsupp.total ι M R v) l = 0
i : ι
hn : ¬↑l i = 0
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i (↑l i) - l) = ↑l i • v i
simp [hl]