no goals
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1419247
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ ↑(toLin v₁ v₂) (↑(toMatrix v₁ v₂) f) = f
rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]