-- Mathlib/Algebra/Lie/Derivation/Basic.lean
theorem iterate_apply_lie (D : LieDerivation R L L) (n : ℕ) (a b : L) :
    D^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, choose n ij.1 • ⁅D^[ij.1] a, D^[ij.2] b⁆

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).1 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆ =
    n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆

Tactic:
rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]

Result:
no goals

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ ∑ x ∈ antidiagonal n, n.choose x.1 • ⁅D ((⇑D)^[x.1] a), (⇑D)^[x.2] b⁆ =
    ∑ x ∈ antidiagonal n, n.choose x.2 • ⁅D ((⇑D)^[x.1] a), (⇑D)^[x.2] b⁆

Tactic:
refine sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_

Result:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).1 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆ =
    n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]
  simp only [Function.iterate_succ_apply', ih, map_sum, map_nsmul, apply_lie_eq_add, smul_add,
    sum_add_distrib, add_right_inj]
  refine sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_
  rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]

Result:
no goals

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2 + 1] b⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅(⇑D)^[ij.1 + 1] a, (⇑D)^[ij.2] b⁆

Tactic:
simp only [Function.iterate_succ_apply', ih, map_sum, map_nsmul, apply_lie_eq_add, smul_add,
  sum_add_distrib, add_right_inj]

Result:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ ∑ x ∈ antidiagonal n, n.choose x.1 • ⁅D ((⇑D)^[x.1] a), (⇑D)^[x.2] b⁆ =
    ∑ x ∈ antidiagonal n, n.choose x.2 • ⁅D ((⇑D)^[x.1] a), (⇑D)^[x.2] b⁆

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ = ∑ ij ∈ antidiagonal (n + 1), (n + 1).choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]

Result:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2 + 1] b⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅(⇑D)^[ij.1 + 1] a, (⇑D)^[ij.2] b⁆

Proof state:
case zero
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ (⇑D)^[0] ⁅a, b⁆ = ∑ ij ∈ antidiagonal 0, Nat.choose 0 ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
simp

Result:
no goals