-- Module: Mathlib.LinearAlgebra.TensorProduct.Matrix
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
rw :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₁ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₂ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2)
      ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A))
      ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₃ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A
      ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₄ rw₅ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')

Tactic:
rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]

Premises used: LinearEquiv.eq_symm_apply, Matrix.toLin_symm, TensorProduct.toMatrix_map, LinearMap.toMatrix_toLin