{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          {motive : Coalgebra R A → Sort u_1} →
            (t : Coalgebra R A) →
              ([toCoalgebraStruct : CoalgebraStruct R A] →
                  (coassoc :
                      ↑(TensorProduct.assoc R A A A) ∘ₗ
                          LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
                        LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul) →
                    (rTensor_counit_comp_comul :
                        LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul =
                          (TensorProduct.mk R R A) 1) →
                      (lTensor_counit_comp_comul :
                          LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul =
                            (TensorProduct.mk R A R).flip 1) →
                        motive
                          { toCoalgebraStruct := toCoalgebraStruct, coassoc := coassoc,
                            rTensor_counit_comp_comul := rTensor_counit_comp_comul,
                            lTensor_counit_comp_comul := lTensor_counit_comp_comul }) →
                motive t