∀ {R : Type u_2} [inst : CommSemiring R] (A : Type u_1) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (B : Type u_3)
  (C : Type u_4) [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra A C] [IsScalarTower R A C],
  TensorProduct.CompatibleSMul A R B C