∀ (R : Type uR) (S : Type uS) (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A],
  (Algebra.TensorProduct.rid R S A).toLinearEquiv = TensorProduct.AlgebraTensorModule.rid R S A