no goals
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_5
R : Type u_4
M : Type u_7
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.410998
M₂ : Type ?u.411001
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ Basis.toMatrix c ↑c' ⬝ ↑(toMatrix b' c') f ⬝ Basis.toMatrix b' ↑b = ↑(toMatrix b c) f
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]