no goals
ι : Type u_2
ι' : Type ?u.168945
R : Type u_1
R₂ : Type ?u.168951
K : Type ?u.168954
M : Type u_3
M' : Type ?u.168960
M'' : Type ?u.168963
V : Type u
V' : Type ?u.168968
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
⊢ ↑(sumCoords b) (↑b i) = 1
simp only [Basis.sumCoords, LinearMap.id_coe, LinearEquiv.coe_coe, id.def, Basis.repr_self,
  Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp, Finsupp.sum_single_index]