no goals
R : Type u_2
inst✝⁹ : CommSemiring R
l : Type ?u.2458702
m : Type ?u.2458705
n : Type u_1
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.2458729
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2459231
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
M : Matrix n n R
v : M₁
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₁)) (↑(↑toLinAlgEquiv' M) ↑(↑v₁.repr v)) =
    ∑ j : n, mulVec M (↑(↑v₁.repr v)) j • ↑v₁ j
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]