∀ (R : Type u_2) (S : Type u_3) (A : Type u_1) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A]
  (x y : TensorProduct R A R),
  (Coalgebra.TensorProduct.rid R S A).toFun (x * y) =
    (Coalgebra.TensorProduct.rid R S A).toFun x * (Coalgebra.TensorProduct.rid R S A).toFun y