no goals
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι × ι'
⊢ ↑(↑(smul b c).repr x) ij = ↑(↑b.repr (↑(↑c.repr x) ij.snd)) ij.fst
simp [Basis.smul]