∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N →ₗ[R] P),
  LinearMap.lTensor Q g = ↑(TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N)