no goals
ι : Type u_1
ι' : Type ?u.843940
R : Type u_2
R₂ : Type ?u.843946
K : Type ?u.843949
M : Type u_3
M' : Type ?u.843955
M'' : Type ?u.843958
V : Type u
V' : Type ?u.843963
v : ι → M
inst✝⁸ : Ring R
inst✝⁷ : CommRing R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup M''
inst✝³ : Module R M
inst✝² : Module R₂ M
inst✝¹ : Module R M'
inst✝ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i j : ι
h : j ≠ i
⊢ ↑(↑(LinearIndependent.repr hli) { val := v j, property := (_ : v j ∈ ↑(span R (Set.range v))) }) i = 0
simp [hli.repr_eq_single j, h]