case h
ι : Type u_1
ι' : Type ?u.163708
R : Type u_2
R₂ : Type ?u.163714
K : Type ?u.163717
M : Type u_3
M' : Type ?u.163723
M'' : Type ?u.163726
V : Type u
V' : Type ?u.163731
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
inst✝ : Fintype ι
m : M
⊢ ↑(sumCoords b) m = ↑(∑ i : ι, coord b i) m
ι : Type u_1
ι' : Type ?u.163708
R : Type u_2
R₂ : Type ?u.163714
K : Type ?u.163717
M : Type u_3
M' : Type ?u.163723
M'' : Type ?u.163726
V : Type u
V' : Type ?u.163731
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
inst✝ : Fintype ι
⊢ ↑(sumCoords b) = ↑(∑ i : ι, coord b i)
ext m
no goals
case h
ι : Type u_1
ι' : Type ?u.163708
R : Type u_2
R₂ : Type ?u.163714
K : Type ?u.163717
M : Type u_3
M' : Type ?u.163723
M'' : Type ?u.163726
V : Type u
V' : Type ?u.163731
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
inst✝ : Fintype ι
m : M
⊢ ↑(sumCoords b) m = ↑(∑ i : ι, coord b i) m
simp only [sumCoords, Finsupp.sum_fintype, LinearMap.id_coe, LinearEquiv.coe_coe, coord_apply,
  id.def, Fintype.sum_apply, imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, comp_apply,
  LinearMap.coeFn_sum]