-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
z : M
n : ℕ
ih :
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                  (a : M) → M)
                z) :
            M) :
      M)
succ :
  ∀ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HSMul.hSMul (β := M) (n.choose x_1.1)
        (Bracket.bracket (L := L)
            ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
                ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                      (a : L) → L)
                    y :
                  L) :
              L)
            ((HPow.hPow (α := Module.End R M)
                  (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) x_1.2 :
                (a : M) → M)
              z) :
          M) =
      HSMul.hSMul (β := M) (n.choose x_1.2)
        (Bracket.bracket (L := L)
            ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
                ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                      (a : L) → L)
                    y :
                  L) :
              L)
            ((HPow.hPow (α := Module.End R M)
                  (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) x_1.2 :
                (a : M) → M)
              z) :
          M)
⊢ HAdd.hAdd (α := M)
      (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose x_1.1)
          (Bracket.bracket (L := L)
              ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
                  ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                        (a : L) → L)
                      y :
                    L) :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
                    x_1.2 :
                  (a : M) → M)
                z) :
            M))
      (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose x_1.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                    (a : L) → L)
                  y :
                L)
              (((((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
                  (a : M) → M)
                ((HPow.hPow (α := Module.End R M)
                        (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
                        x_1.2 :
                      (a : M) → M)
                    z :
                  M)) :
            M)) =
    HAdd.hAdd (α := M)
      (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose x_1.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                    (a : L) → L)
                  y :
                L)
              (((((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
                  (a : M) → M)
                ((HPow.hPow (α := Module.End R M)
                        (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
                        x_1.2 :
                      (a : M) → M)
                    z :
                  M)) :
            M))
      (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose x_1.2)
          (Bracket.bracket (L := L)
              ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
                  ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) x_1.1 :
                        (a : L) → L)
                      y :
                    L) :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
                    x_1.2 :
                  (a : M) → M)
                z) :
            M))

Tactic:
rw [add_comm, add_left_cancel_iff, sum_congr rfl]

Premises used: add_left_cancel_iff, add_comm, Finset.sum_congr, rfl