no goals
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2626461
m : Type ?u.2626464
n : Type u_3
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type ?u.2626488
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.2626990
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f g : M₁ →ₗ[R] M₁
⊢ ↑(toMatrixAlgEquiv v₁) (comp f g) = ↑(toMatrixAlgEquiv v₁) f ⬝ ↑(toMatrixAlgEquiv v₁) g
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]