∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_3} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (g : N →ₚₗ[R] P) (f : M →ₚₗ[R] N) {S : Type u_1} [inst_7 : CommSemiring S] [inst_8 : Algebra R S] {S' : Type u_1}
  [inst_9 : CommSemiring S'] [inst_10 : Algebra R S'] (φ : S →ₐ[R] S'),
  ⇑(LinearMap.rTensor P φ.toLinearMap) ∘ g.toFun' S ∘ f.toFun' S =
    (g.toFun' S' ∘ f.toFun' S') ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)