∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Bialgebra R A],
  (LinearMap.mul R A).compr₂ CoalgebraStruct.counit =
    (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit