no goals
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι × κ
⊢ ↑(tensorProduct b c) i = ↑b i.fst ⊗ₜ[R] ↑c i.snd
simp [Basis.tensorProduct]