no goals
R : Type u_3
M : Type u_6
N : Type u_7
P : Type ?u.79666
M' : Type u_8
N' : Type u_9
ι : Type u_2
κ : Type u_5
τ : Type ?u.79681
ι' : Type u_1
κ' : Type u_4
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ ↑(toLin (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (kroneckerMap (fun x x_1 => x * x_1) A B) =
    TensorProduct.map (↑(toLin bM bM') A) (↑(toLin bN bN') B)
rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
  toMatrix_toLin]