∀ (R : Type u_2) (A : Type u_1) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A],
  TensorProduct.map LinearMap.id LinearMap.id ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.id