awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
have 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)
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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((D1 : (a : L) → M) x : M) ((D2 : (a : L) → M) x : M)
have 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)
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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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⁆
⊢ (⇑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⁆
have 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⁆)
Tactic: rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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⁆
⊢ (⇑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⁆)
have 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))
Tactic: simp only [Function.iterate_succ_apply', ih, map_sum, map_nsmul, apply_lie_eq_add, smul_add,
      sum_add_distrib, add_right_inj]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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))
have 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)
Tactic: refine sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
⊢ (⇑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⁆
have 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⁆
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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⁆
⊢ (⇑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⁆
have 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⁆
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
⊢ (⇑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⁆
have 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⁆)
Tactic: rw [iterate_apply_lie D n a b]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 : LieDerivation R L L
a b : L
⊢ (⁅(↑D1 : L →ₗ[R] L), (↑D2 : L →ₗ[R] L)⁆ : (a : L) → L) ⁅a, b⁆ =
    HSub.hSub (α := L) (β := L) (⁅a, (⁅(↑D1 : L →ₗ[R] L), (↑D2 : L →ₗ[R] L)⁆ : (a : L) → L) b⁆ : L)
      (⁅b, (⁅(↑D1 : L →ₗ[R] L), (↑D2 : L →ₗ[R] L)⁆ : (a : L) → L) a⁆ : L)
have simp : HAdd.hAdd (α := L) (β := L) (⁅a, (D1 : (a : L) → L) ((D2 : (a : L) → L) b : L)⁆ : L)
        (Bracket.bracket (L := L) ((D1 : (a : L) → L) a : L) ((D2 : (a : L) → L) b) : L) +
      HAdd.hAdd (α := L) (Bracket.bracket (L := L) ((D2 : (a : L) → L) a : L) ((D1 : (a : L) → L) b) : L)
        (Bracket.bracket (L := L) ((D1 : (a : L) → L) ((D2 : (a : L) → L) a : L) : L) b) -
    (HAdd.hAdd (α := L) (β := L) (⁅a, (D2 : (a : L) → L) ((D1 : (a : L) → L) b : L)⁆ : L)
        (Bracket.bracket (L := L) ((D2 : (a : L) → L) a : L) ((D1 : (a : L) → L) b) : L) +
      HAdd.hAdd (α := L) (Bracket.bracket (L := L) ((D1 : (a : L) → L) a : L) ((D2 : (a : L) → L) b) : L)
        (Bracket.bracket (L := L) ((D2 : (a : L) → L) ((D1 : (a : L) → L) a : L) : L) b)) =
  HSub.hSub (α := L) (β := L) (⁅a, (D1 : (a : L) → L) ((D2 : (a : L) → L) b : L)⁆ : L)
      (⁅a, (D2 : (a : L) → L) ((D1 : (a : L) → L) b : L)⁆ : L) -
    -(Bracket.bracket (L := L) ((D1 : (a : L) → L) ((D2 : (a : L) → L) a : L) : L) b -
        Bracket.bracket (L := L) ((D2 : (a : L) → L) ((D1 : (a : L) → L) a : L) : L) b)
Tactic: simp only [Ring.lie_def, apply_lie_eq_add, coeFn_coe,
      LinearMap.sub_apply, Module.End.mul_apply, map_add, sub_lie, lie_sub, ← lie_skew b]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆
have H : ∀ (a : L), Eq (α := L) ((⁅d + e, f⁆ : (a : L) → L) a : L) ((⁅d, f⁆ + ⁅e, f⁆ : (a : L) → L) a : L)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
a : L
⊢ Eq (α := L) ((⁅d + e, f⁆ : (a : L) → L) a : L) ((⁅d, f⁆ + ⁅e, f⁆ : (a : L) → L) a : L)
have H : HAdd.hAdd (α := L) (β := L) ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L)
      ((e : (a : L) → L) ((f : (a : L) → L) a : L) : L) -
    HAdd.hAdd (α := L) (β := L) ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L)
      ((f : (a : L) → L) ((e : (a : L) → L) a : L) : L) =
  HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L)
      ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L) +
    HSub.hSub (α := L) (β := L) ((e : (a : L) → L) ((f : (a : L) → L) a : L) : L)
      ((f : (a : L) → L) ((e : (a : L) → L) a : L) : L)
Tactic: simp only [commutator_apply, add_apply, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆
have H : ∀ (a : L), Eq (α := L) ((⁅d, e + f⁆ : (a : L) → L) a : L) ((⁅d, e⁆ + ⁅d, f⁆ : (a : L) → L) a : L)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
a : L
⊢ Eq (α := L) ((⁅d, e + f⁆ : (a : L) → L) a : L) ((⁅d, e⁆ + ⁅d, f⁆ : (a : L) → L) a : L)
have H : HAdd.hAdd (α := L) (β := L) ((d : (a : L) → L) ((e : (a : L) → L) a : L) : L)
      ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L) -
    HAdd.hAdd (α := L) (β := L) ((e : (a : L) → L) ((d : (a : L) → L) a : L) : L)
      ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L) =
  HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((e : (a : L) → L) a : L) : L)
      ((e : (a : L) → L) ((d : (a : L) → L) a : L) : L) +
    HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L)
      ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L)
Tactic: simp only [commutator_apply, add_apply, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d : LieDerivation R L L
⊢ ⁅d, d⁆ = 0
have H : ∀ (a : L), Eq (α := L) ((⁅d, d⁆ : (a : L) → L) a : L) ((0 : (a : L) → L) a : L)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d : LieDerivation R L L
a : L
⊢ Eq (α := L) ((⁅d, d⁆ : (a : L) → L) a : L) ((0 : (a : L) → L) a : L)
have H : HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((d : (a : L) → L) a : L) : L)
    ((d : (a : L) → L) ((d : (a : L) → L) a : L) : L) =
  0
Tactic: simp only [commutator_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆
have H : ∀ (a : L), Eq (α := L) ((⁅d, ⁅e, f⁆⁆ : (a : L) → L) a : L) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : L) → L) a : L)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
a : L
⊢ Eq (α := L) ((⁅d, ⁅e, f⁆⁆ : (a : L) → L) a : L) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : L) → L) a : L)
have H : HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((e : (a : L) → L) ((f : (a : L) → L) a : L) : L) : L)
      ((d : (a : L) → L) ((f : (a : L) → L) ((e : (a : L) → L) a : L) : L) : L) -
    HSub.hSub (α := L) (β := L) ((e : (a : L) → L) ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L) : L)
      ((f : (a : L) → L) ((e : (a : L) → L) ((d : (a : L) → L) a : L) : L) : L) =
  HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((e : (a : L) → L) ((f : (a : L) → L) a : L) : L) : L)
        ((e : (a : L) → L) ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L) : L) -
      HSub.hSub (α := L) (β := L) ((f : (a : L) → L) ((d : (a : L) → L) ((e : (a : L) → L) a : L) : L) : L)
        ((f : (a : L) → L) ((e : (a : L) → L) ((d : (a : L) → L) a : L) : L) : L) +
    (HSub.hSub (α := L) (β := L) ((e : (a : L) → L) ((d : (a : L) → L) ((f : (a : L) → L) a : L) : L) : L)
        ((e : (a : L) → L) ((f : (a : L) → L) ((d : (a : L) → L) a : L) : L) : L) -
      HSub.hSub (α := L) (β := L) ((d : (a : L) → L) ((f : (a : L) → L) ((e : (a : L) → L) a : L) : L) : L)
        ((f : (a : L) → L) ((d : (a : L) → L) ((e : (a : L) → L) a : L) : L) : L))
Tactic: simp only [commutator_apply, add_apply, map_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D1 D2 : LieDerivation R L L
r : R
d e : LieDerivation R L L
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆
have H : ∀ (a : L), Eq (α := L) ((⁅d, r • e⁆ : (a : L) → L) a : L) ((r • ⁅d, e⁆ : (a : L) → L) a : L)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
m n : M
⊢ (let __spread.0 : L →ₗ[R] M :=
      (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) (m + n);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    HAdd.hAdd (α := LieDerivation R L M)
      (let __spread.0 : L →ₗ[R] M :=
        (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m;
      { toLinearMap := __spread.0, leibniz' := ⋯ : LieDerivation R L M })
      (let __spread.0 : L →ₗ[R] M :=
        (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) n;
      { toLinearMap := __spread.0, leibniz' := ⋯ : LieDerivation R L M })
have H : ∀ (a : L),
  Eq.{u_3 + 1} (α := M)
    ((let __spread.0 : L →ₗ[R] M :=
            (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) (m + n);
          { toLinearMap := __spread.0, leibniz' := sorry } :
          (a : L) → M)
        a :
      M)
    ((HAdd.hAdd (α := LieDerivation R L M)
            (let __spread.0 : L →ₗ[R] M :=
              (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m;
            { toLinearMap := __spread.0, leibniz' := sorry : LieDerivation R L M })
            (let __spread.0 : L →ₗ[R] M :=
              (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) n;
            { toLinearMap := __spread.0, leibniz' := sorry : LieDerivation R L M }) :
          (a : L) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
t : R
m : M
⊢ (let __spread.0 : L →ₗ[R] M :=
      (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) (t • m);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    HSMul.hSMul (α := R) (β := LieDerivation R L M) ((RingHom.id R : (a : R) → R) t : R)
      (let __spread.0 : L →ₗ[R] M :=
        (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m;
      { toLinearMap := __spread.0, leibniz' := ⋯ : LieDerivation R L M })
have H : ∀ (a : L),
  Eq.{u_3 + 1} (α := M)
    ((let __spread.0 : L →ₗ[R] M :=
            (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) (t • m);
          { toLinearMap := __spread.0, leibniz' := sorry } :
          (a : L) → M)
        a :
      M)
    ((HSMul.hSMul (α := R) (β := LieDerivation R L M) ((RingHom.id R : (a : R) → R) t : R)
            (let __spread.0 : L →ₗ[R] M :=
              (LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m;
            { toLinearMap := __spread.0, leibniz' := sorry : LieDerivation R L M }) :
          (a : L) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
x : L
D : LieDerivation R L M
⊢ ⁅x, (↑D : L →ₗ[R] M)⁆ = (↑⁅x, D⁆ : L →ₗ[R] M)
have h : ∀ (x_1 : L),
  Eq.{u_3 + 1} (α := M) ((⁅x, (↑D : L →ₗ[R] M)⁆ : (a : L) → M) x_1 : M) (((↑⁅x, D⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅t • x, D⁆ = t • ⁅x, D⁆
have H : ∀ (a : L), Eq.{u_3 + 1} (α := M) ((⁅t • x, D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅x, t • D⁆ = t • ⁅x, D⁆
have H : ∀ (a : L), Eq.{u_3 + 1} (α := M) ((⁅x, t • D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆
have H : ∀ (y : L), Eq (α := L) ((⁅x, ⁅D₁, D₂⁆⁆ : (a : L) → L) y : L) ((⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ : (a : L) → L) y : L)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
⊢ ∀ {x y : L},
    (IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun ⁅x, y⁆ =
      ⁅(IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun x, (IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun y⁆
have this : SMulCommClass R L L
Tactic: have : SMulCommClass R L L := LieAlgebra.smulCommClass R L