-- 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 : ℕ
zero :
  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) 0 :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
        HSMul.hSMul (β := M) (Nat.choose 0 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 :
  ∀ (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)),
    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 + 1) :
            (a : M) → M)
          ⁅y, z⁆ :
        M)
      (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ (n + 1),
          HSMul.hSMul (β := M) ((n + 1).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)
⊢ 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)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_antidiagonal_choose_succ_nsmul
      (fun i j ↦ ⁅((ad R L x) ^ i) y, ((φ x) ^ j) z⁆) n]
    simp only [pow_succ', Module.End.mul_apply, ih, map_sum, map_nsmul,
      toEnd_lie, nsmul_add, sum_add_distrib]
    rw [add_comm, add_left_cancel_iff, sum_congr rfl]
    rintro ⟨i, j⟩ hij
    rw [mem_antidiagonal] at hij
    rw [Nat.choose_symm_of_eq_add hij.symm]

Premises used: Finset.sum_add_distrib, map_sum, add_left_cancel_iff, add_comm, LieModule.toEnd_lie, nsmul_add, Finset.HasAntidiagonal.mem_antidiagonal, Module.End.mul_apply, map_nsmul, Finset.sum_congr, pow_succ', rfl