∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : CoalgebraStruct R A} {a : A} {ι : Type u_1} {index : Finset ι} {left right : ι → A}
  {eq : ∑ i ∈ index, left i ⊗ₜ[R] right i = CoalgebraStruct.comul a} {ι_1 : Type u_1} {index_1 : Finset ι_1}
  {left_1 right_1 : ι_1 → A} {eq_1 : ∑ i ∈ index_1, left_1 i ⊗ₜ[R] right_1 i = CoalgebraStruct.comul a},
  { ι := ι, index := index, left := left, right := right, eq := eq } =
      { ι := ι_1, index := index_1, left := left_1, right := right_1, eq := eq_1 } →
    ι = ι_1 ∧ index ≍ index_1 ∧ left ≍ left_1 ∧ right ≍ right_1