no goals
ι : Type u_2
ι' : Type ?u.820992
R : Type u_3
R₂ : Type ?u.820998
K : Type ?u.821001
M : Type u_1
M' : Type ?u.821007
M'' : Type ?u.821010
V : Type u
V' : Type ?u.821015
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 : ι
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i 1) = v i
simp