no goals
R : Type u_3
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ ↑(leftMulMatrix (Basis.smul b c)) x ik jk = ↑(leftMulMatrix b) (↑(leftMulMatrix c) x ik.snd jk.snd) ik.fst jk.fst
simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smul_apply,
  Basis.smul_repr, Finsupp.smul_apply, id.smul_eq_mul, LinearEquiv.map_smul, mul_smul_comm,
  coe_lmul_eq_mul, LinearMap.mul_apply']