Commutator bracket through a Sweedler representation

Evaluation of the ring commutator ⁅f, g⁆ of the convolution algebra WithConv (C →ₗ[R] A) through a Sweedler representation. [UPSTREAM] candidate for Mathlib.RingTheory.Coalgebra.Convolution, beside Coalgebra.Repr.convMul_apply.

theorem Coalgebra.Repr.lie_apply {R : Type u_1} [CommSemiring R] {C : Type u_2} [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_3} {a : C} {A : Type u_4} [Ring A] [Algebra R A] (𝓡 : Repr R a ι) (f g : WithConv (C →ₗ[R] A)) : ⁅f, g⁆.ofConv a = ∑ i ∈ 𝓡.index, (f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i) - g.ofConv (𝓡.left i) * f.ofConv (𝓡.right i))

The ring commutator bracket on the convolution algebra, evaluated through a Sweedler representation.