{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [toHopfAlgebraStruct : HopfAlgebraStruct R A] →
          LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
              Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit →
            LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
                Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit →
              HopfAlgebra R A