no goals
R : Type u_3
inst✝⁷ : CommSemiring R
l : Type ?u.1631986
m : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_4
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 : Matrix m n R
v : M₁
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₂)) (↑(↑toLin' M) ↑(↑v₁.repr v)) = ∑ j : m, mulVec M (↑(↑v₁.repr v)) j • ↑v₂ j
rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]