no goals
ι : Type u_1
ι' : Type u_2
κ : Type ?u.628277
κ' : Type ?u.628280
R : Type u_3
M : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
R₂ : Type ?u.628473
M₂ : Type ?u.628476
inst✝⁶ : CommRing R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type ?u.629221
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✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ toMatrix b ↑b' ⬝ toMatrix b' ↑b = 1
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]