∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R N M),
  (TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R₂ N₂ M₂) ((TensorProduct.map g f) x)