ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
⊢ i = j
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v
intro i j hij
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
⊢ i = j
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
⊢ i = j
let l : ι →₀ R := Finsupp.single i (1 : R) - Finsupp.single j 1
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
⊢ i = j
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
⊢ i = j
have h_total : Finsupp.total ι M R v l = 0 := by
  simp_rw [LinearMap.map_sub, Finsupp.total_apply]
  simp [hij]
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
h_single_eq : Finsupp.single i 1 = Finsupp.single j 1
⊢ i = j
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
⊢ i = j
have h_single_eq : Finsupp.single i (1 : R) = Finsupp.single j 1 := by
  rw [linearIndependent_iff] at hv
  simp [eq_add_of_sub_eq' (hv l h_total)]
no goals
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
h_single_eq : Finsupp.single i 1 = Finsupp.single j 1
⊢ i = j
simpa [Finsupp.single_eq_single_iff] using h_single_eq
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
⊢ ((Finsupp.sum (Finsupp.single i 1) fun i a => a • v i) - Finsupp.sum (Finsupp.single j 1) fun i a => a • v i) = 0
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
⊢ ↑(Finsupp.total ι M R v) l = 0
simp_rw [LinearMap.map_sub, Finsupp.total_apply]
no goals
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
⊢ ((Finsupp.sum (Finsupp.single i 1) fun i a => a • v i) - Finsupp.sum (Finsupp.single j 1) fun i a => a • v i) = 0
simp [hij]
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : ∀ (l : ι →₀ R), ↑(Finsupp.total ι M R v) l = 0 → l = 0
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
⊢ Finsupp.single i 1 = Finsupp.single j 1
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
⊢ Finsupp.single i 1 = Finsupp.single j 1
rw [linearIndependent_iff] at hv
no goals
ι : Type u'
ι' : Type ?u.231997
R : Type u_1
K : Type ?u.232003
M : Type u_2
M' : Type ?u.232009
M'' : Type ?u.232012
V : Type u
V' : Type ?u.232017
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
inst✝ : Nontrivial R
hv : ∀ (l : ι →₀ R), ↑(Finsupp.total ι M R v) l = 0 → l = 0
i j : ι
hij : v i = v j
l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1
h_total : ↑(Finsupp.total ι M R v) l = 0
⊢ Finsupp.single i 1 = Finsupp.single j 1
simp [eq_add_of_sub_eq' (hv l h_total)]