case h
ι : Type u_3
ι' : Type ?u.157559
R : Type u_1
R₂ : Type ?u.157565
K : Type ?u.157568
M : Type u_2
M' : Type ?u.157574
M'' : Type ?u.157577
V : Type u
V' : Type ?u.157582
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 : M
⊢ ↑(sumCoords b) m = ∑ᶠ (i : ι), ↑(coord b i) m
ι : Type u_3
ι' : Type ?u.157559
R : Type u_1
R₂ : Type ?u.157565
K : Type ?u.157568
M : Type u_2
M' : Type ?u.157574
M'' : Type ?u.157577
V : Type u
V' : Type ?u.157582
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) = fun m => ∑ᶠ (i : ι), ↑(coord b i) m
ext m
no goals
case h
ι : Type u_3
ι' : Type ?u.157559
R : Type u_1
R₂ : Type ?u.157565
K : Type ?u.157568
M : Type u_2
M' : Type ?u.157574
M'' : Type ?u.157577
V : Type u
V' : Type ?u.157582
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 : M
⊢ ↑(sumCoords b) m = ∑ᶠ (i : ι), ↑(coord b i) m
simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe,
  LinearEquiv.coe_coe, Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp,
  finsum_eq_sum _ (b.repr m).finite_support, Finsupp.sum, Finset.finite_toSet_toFinset, id.def,
  Finsupp.fun_support_eq]