awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap : L →ₗ[R] M
leibniz' :
  ∀ (a b : L),
    (toLinearMap : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M)
toLinearMap_1 : L →ₗ[R] M
leibniz'_1 :
  ∀ (a b : L),
    (toLinearMap_1 : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap_1 : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap_1 : (a : L) → M) a⁆ : M)
h :
  Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
    ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 })
mk : toLinearMap = toLinearMap_1
⊢ Eq (α := LieDerivation R L M) { toLinearMap := toLinearMap, leibniz' := leibniz' }
    { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap : L →ₗ[R] M
leibniz' :
  ∀ (a b : L),
    (toLinearMap : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M)
toLinearMap_1 : L →ₗ[R] M
leibniz'_1 :
  ∀ (a b : L),
    (toLinearMap_1 : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap_1 : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap_1 : (a : L) → M) a⁆ : M)
h :
  Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
    ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 })
⊢ toLinearMap = toLinearMap_1

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap : L →ₗ[R] M
leibniz' :
  ∀ (a b : L),
    (toLinearMap : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap : (a : L) → M) a⁆ : M)
toLinearMap_1 : L →ₗ[R] M
leibniz'_1 :
  ∀ (a b : L),
    (toLinearMap_1 : (a : L) → M) ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M) (⁅a, (toLinearMap_1 : (a : L) → M) b⁆ : M) (⁅b, (toLinearMap_1 : (a : L) → M) a⁆ : M)
h :
  Eq (α := (a : L) → M) ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap, leibniz' := leibniz' })
    ((fun (D : LieDerivation R L M) ↦ D.toFun) { toLinearMap := toLinearMap_1, leibniz' := leibniz'_1 })
⊢ toLinearMap = toLinearMap_1

Tactic:
exact DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D : LieDerivation R L M
⊢ D.toFun = (⇑D : (a : L) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
f : L →ₗ[R] M
h₁ :
  ∀ (a b : L),
    (f : (a : L) → M) ⁅a, b⁆ = HSub.hSub (α := M) (β := M) (⁅a, (f : (a : L) → M) b⁆ : M) (⁅b, (f : (a : L) → M) a⁆ : M)
⊢ Eq (α := (a : L) → M) (⇑{ toLinearMap := f, leibniz' := h₁ } : (a : L) → M) (⇑f : (a : L) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
f : LieDerivation R L M
⊢ Eq (α := (a : L) → M) (⇑(↑f : L →ₗ[R] M) : (a : L) → M) (⇑f : (a : L) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
⊢ Function.Injective (α := LieDerivation R L M) (β := L → M) (DFunLike.coe (β := fun (a : L) ↦ M))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
H : ∀ (a : L), Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) a : M) ((D2 : (a : L) → M) a : M)
⊢ D1 = D2

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
h : D1 = D2
a : L
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) a : M) ((D2 : (a : L) → M) a : M)

Tactic:
DFunLike.congr_fun h a

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D : LieDerivation R L M
a b : L
⊢ (D : (a : L) → M) ⁅a, b⁆ = HSub.hSub (α := M) (β := M) (⁅a, (D : (a : L) → M) b⁆ : M) (⁅b, (D : (a : L) → M) a⁆ : M)

Tactic:
D.leibniz' a b

Premises used: LieDerivation.leibniz'
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
rw :
  HSub.hSub (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (⁅b, (D : (a : L) → L) a⁆ : L) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
rw₁ :
  HAdd.hAdd (α := L) (β := L) (⁅a, (D : (a : L) → L) b⁆ : L) (-⁅b, (D : (a : L) → L) a⁆ : L) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
rw₂ rw₃ :
  HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b) =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)
⊢ (D : (a : L) → L) ⁅a, b⁆ =
    HAdd.hAdd (α := L) (⁅a, (D : (a : L) → L) b⁆ : L) (Bracket.bracket (L := L) ((D : (a : L) → L) a : L) b)

Tactic:
rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]

Premises used: sub_eq_add_neg, lie_skew, LieDerivation.apply_lie_eq_sub
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x_1 x : L
hx : x ∈ s
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)

Tactic:
h hx
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x_1 x : L
hx : x ∈ s
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)

Tactic:
exact h hx
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x : L
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) 0 : M) ((D2 : (a : L) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x_1 x y : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
hy_1 : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) y
hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
hy : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) y : M) ((D2 : (a : L) → M) y : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) (x + y) : M) ((D2 : (a : L) → M) (x + y) : M)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x_1 : L
t : R
x : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) (t • x) : M) ((D2 : (a : L) → M) (t • x) : M)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x_1 x y : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
hy_1 : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) y
hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
hy : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) y : M) ((D2 : (a : L) → M) y : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) ⁅x, y⁆ : M) ((D2 : (a : L) → M) ⁅x, y⁆ : M)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
x : L
hx : x ∈ (↑(LieSubalgebra.lieSpan R L s) : Set L)
mem : ∀ (x : L) (hx : x ∈ s), Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
zero : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) 0 : M) ((D2 : (a : L) → M) 0 : M)
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x →
      Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) y →
        ∀ (hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M))
          (hy : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) y : M) ((D2 : (a : L) → M) y : M)),
          Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) (x + y) : M) ((D2 : (a : L) → M) (x + y) : M)
smul :
  ∀ (t : R) (x : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x →
      ∀ (hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)),
        Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) (t • x) : M) ((D2 : (a : L) → M) (t • x) : M)
lie :
  ∀ (x y : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x →
      Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) y →
        ∀ (hx : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M))
          (hy : Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) y : M) ((D2 : (a : L) → M) y : M)),
          Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) ⁅x, y⁆ : M) ((D2 : (a : L) → M) ⁅x, y⁆ : M)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)

Tactic:
induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D1 D2 : LieDerivation R L M
s : Set L
hs : Eq (α := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) ⊤
h : Set.EqOn.{u_2, u_3} (β := M) (⇑D1 : (a : L) → M) (⇑D2 : (a : L) → M) s
⊢ D1 = D2

Tactic:
ext fun _ => eqOn_lieSpan h <| hs.symm ▸ trivial

Premises used: trivial, Eq.rec, LieDerivation.eqOn_lieSpan, LieDerivation.ext, Eq.symm
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ (⇑D : (a : L) → L)^[0] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0,
      Nat.choose 0 ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih :
  (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
succ :
  (⇑D : (a : L) → L)^[n + 1] ⁅a, b⁆ =
    HAdd.hAdd (α := L)
      (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
        n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2 + 1] b⁆)
      (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
        n.choose ij.2 • ⁅(⇑D : (a : L) → L)^[ij.1 + 1] a, (⇑D : (a : L) → L)^[ij.2] b⁆)
⊢ (⇑D : (a : L) → L)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (n + 1).choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆

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

Premises used: Finset.sum_antidiagonal_choose_succ_nsmul, Bracket.bracket, Nat.iterate, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih :
  (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
succ :
  Eq.{u_2 + 1} (α := L)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.1 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.2 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))
⊢ (⇑D : (a : L) → L)^[n + 1] ⁅a, b⁆ =
    HAdd.hAdd (α := L)
      (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
        n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2 + 1] b⁆)
      (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
        n.choose ij.2 • ⁅(⇑D : (a : L) → L)^[ij.1 + 1] a, (⇑D : (a : L) → L)^[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]

Premises used: Function.iterate_succ_apply', LieDerivation.apply_lie_eq_add, Finset.sum_add_distrib, map_sum, map_nsmul, add_right_inj, smul_add
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih :
  (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
⊢ Eq.{u_2 + 1} (α := L)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.1 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.2 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))

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

Premises used: Nat.choose, Bracket.bracket, _private.0.LieDerivation.iterate_apply_lie.match_1, Nat.iterate, Prod.fst, HSMul.hSMul, Eq, Prod.snd, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih :
  (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
succ :
  ∀ (x : ℕ × ℕ) (i j : ℕ) (hij : (i, j) ∈ @antidiagonal _ instAddMonoid _ n),
    n.choose (i, j).1 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
          ((⇑D : (a : L) → L)^[(i, j).2] b) =
      n.choose (i, j).2 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
          ((⇑D : (a : L) → L)^[(i, j).2] b)
⊢ Eq.{u_2 + 1} (α := L)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.1 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose x.2 •
        Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[x.1] a) : L) ((⇑D : (a : L) → L)^[x.2] b))

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih :
  (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ instAddMonoid _ n
succ succ₁ :
  n.choose (i, j).2 •
      Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
        ((⇑D : (a : L) → L)^[(i, j).2] b) =
    n.choose (i, j).2 •
      Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
        ((⇑D : (a : L) → L)^[(i, j).2] b)
⊢ n.choose (i, j).1 •
      Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
        ((⇑D : (a : L) → L)^[(i, j).2] b) =
    n.choose (i, j).2 •
      Bracket.bracket (L := L) ((D : (a : L) → L) ((⇑D : (a : L) → L)^[(i, j).1] a) : L)
        ((⇑D : (a : L) → L)^[(i, j).2] b)

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

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, Eq.symm, Nat.choose_symm_of_eq_add
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
zero :
  (⇑D : (a : L) → L)^[0] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0,
      Nat.choose 0 ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
succ :
  ∀ (n : ℕ)
    (ih :
      (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
        ∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
          n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆),
    (⇑D : (a : L) → L)^[n + 1] ⁅a, b⁆ =
      ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1),
        (n + 1).choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆
⊢ (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[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]

Premises used: Function.iterate_succ_apply', LieDerivation.apply_lie_eq_add, Finset.sum_add_distrib, Finset.sum_antidiagonal_choose_succ_nsmul, Bracket.bracket, map_sum, Nat.iterate, Nat.zero, map_nsmul, Nat.succ, DFunLike.coe, add_right_inj, Finset.sum_congr, smul_add, rfl
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
rw :
  Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆)
    (∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D : (a : L) → L)^[i] a, (⇑D : (a : L) → L)^[n - i] b⁆)
⊢ (⇑D : (a : L) → L)^[n] ⁅a, b⁆ =
    ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D : (a : L) → L)^[i] a, (⇑D : (a : L) → L)^[n - i] b⁆

Tactic:
rw [iterate_apply_lie D n a b]

Premises used: LieDerivation.iterate_apply_lie
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆)
    (∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D : (a : L) → L)^[i] a, (⇑D : (a : L) → L)^[n - i] b⁆)

Tactic:
sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Nat.choose, Bracket.bracket, Nat.iterate, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ Eq.{u_2 + 1} (α := L)
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ n,
      n.choose ij.1 • ⁅(⇑D : (a : L) → L)^[ij.1] a, (⇑D : (a : L) → L)^[ij.2] b⁆)
    (∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D : (a : L) → L)^[i] a, (⇑D : (a : L) → L)^[n - i] b⁆)

Tactic:
exact sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Nat.choose, Bracket.bracket, Nat.iterate, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a_1 b_1 a b : L
⊢ (0 : (a : L) → M) ⁅a, b⁆ = HSub.hSub (α := M) (β := M) (⁅a, (0 : (a : L) → M) b⁆ : M) (⁅b, (0 : (a : L) → M) a⁆ : M)

Tactic:
simp only [LinearMap.zero_apply, lie_zero, sub_self]

Premises used: LinearMap.zero_apply, sub_self, lie_zero
-- Module: Mathlib.Algebra.Lie.Derivation.Basic
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
⊢ Eq (α := (a : L) → M) (⇑0 : (a : L) → M) 0

Tactic:
rfl

Premises used: rfl