no goals
ι : Type u_1
ι' : Type u_4
κ : Type ?u.260003
κ' : Type ?u.260006
R : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.260199
M₂ : Type ?u.260202
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
⊢ ∑ i : ι, toMatrix e v i j • ↑e i = v j
simp_rw [e.toMatrix_apply, e.sum_repr]