no goals
R : Type u_1
R₁ : Type ?u.1290163
R₂ : Type ?u.1290166
M : Type ?u.1290169
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type ?u.1290178
M₂' : Type ?u.1290181
n : Type u_4
m : Type u_5
n' : Type ?u.1290190
m' : Type ?u.1290193
ι : Type ?u.1290196
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
i : n
j : m
⊢ ↑(toMatrix₂ b₁ b₂) B i j = ↑(↑B (↑b₁ i)) (↑b₂ j)
simp only [LinearMap.toMatrix₂, LinearEquiv.trans_apply, LinearMap.toMatrix₂'_apply,
  LinearEquiv.trans_apply, LinearMap.toMatrix₂'_apply, LinearEquiv.arrowCongr_apply,
  Basis.equivFun_symm_stdBasis, LinearEquiv.refl_apply]