∀ (l : Type u_1) (m : Type u_3) (n : Type u_4) (p : Type u_5) (R : Type u_8) (S : Type u_7) (M : Type u_6)
  (N : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module S M] [inst_7 : Module R N]
  [inst_8 : IsScalarTower R S M] [inst_9 : Fintype l] [inst_10 : Fintype m] [inst_11 : Fintype n] [inst_12 : Fintype p]
  [inst_13 : DecidableEq l] [inst_14 : DecidableEq m] [inst_15 : DecidableEq n] [inst_16 : DecidableEq p],
  ((Matrix.liftLinear R) fun ii jj =>
        TensorProduct.AlgebraTensorModule.map (Matrix.singleLinearMap S ii.1 jj.1)
          (Matrix.singleLinearMap R ii.2 jj.2)) ∘ₗ
      TensorProduct.AlgebraTensorModule.lift (Matrix.kroneckerTMulBilinear R S) =
    LinearMap.id