Counit collapse through a Sweedler representation

Applying L ⊗ ε or ε ⊗ L to a Sweedler representation of a recovers L a, for any linear functional L. [UPSTREAM] candidates for Mathlib.RingTheory.Coalgebra.Basic, beside Coalgebra.sum_counit_smul.

theorem Coalgebra.Repr.sum_apply_mul_counit {R : Type u_1} [CommSemiring R] {C : Type u_2} [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_3} {a : C} (𝓡 : Repr R a ι) (L : C →ₗ[R] R) : ∑ i ∈ 𝓡.index, L (𝓡.left i) * counit (𝓡.right i) = L a

Applying L ⊗ ε to a Sweedler representation of a recovers L a.

theorem Coalgebra.Repr.sum_counit_mul_apply {R : Type u_1} [CommSemiring R] {C : Type u_2} [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_3} {a : C} (𝓡 : Repr R a ι) (L : C →ₗ[R] R) : ∑ i ∈ 𝓡.index, counit (𝓡.left i) * L (𝓡.right i) = L a

Applying ε ⊗ L to a Sweedler representation of a recovers L a.