awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
D1 D2 d e f : LieDerivation R L L
a : L
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))
⊢ Eq (α := L) ((⁅d, ⁅e, f⁆⁆ : (a : L) → L) a : L) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : L) → L) a : L)

Tactic:
simp only [commutator_apply, add_apply, map_sub]

Premises used: map_sub, LieDerivation.commutator_apply, LieDerivation.add_apply
-- 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
D1 D2 d e f : LieDerivation R L L
a : L
⊢ 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:
abel
-- 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
D1 D2 : LieDerivation R L L
r : R
d e : LieDerivation R L L
H : ∀ (a : L), Eq (α := L) ((⁅d, r • e⁆ : (a : L) → L) a : L) ((r • ⁅d, e⁆ : (a : L) → L) a : L)
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
ext a
-- 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
D1 D2 : LieDerivation R L L
r : R
d e : LieDerivation R L L
a : L
⊢ Eq (α := L) ((⁅d, r • e⁆ : (a : L) → L) a : L) ((r • ⁅d, e⁆ : (a : L) → L) a : L)

Tactic:
simp only [commutator_apply, map_smul, smul_sub, smul_apply]

Premises used: LieDerivation.commutator_apply, smul_sub, LieDerivation.smul_apply, map_smul
-- 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₁ D₂ : LieDerivation R L L
x : L
⊢ (⁅D₁, D₂⁆ : (a : L) → L) x =
    HSub.hSub (α := L) (β := L) ((D₁ : (a : L) → L) ((D₂ : (a : L) → L) x : L) : L)
      ((D₂ : (a : L) → L) ((D₁ : (a : L) → L) x : L) : L)

Tactic:
rfl

Premises used: 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
D1 D2 : LieDerivation R L L
⊢ (↑(D1 + D2) : L →ₗ[R] L) = (↑D1 : L →ₗ[R] L) + (↑D2 : L →ₗ[R] L)

Tactic:
dsimp
-- 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
D1 : R
D2 : LieDerivation R L L
⊢ (↑(D1 • D2) : L →ₗ[R] L) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) D1 : R) (↑D2 : L →ₗ[R] L)

Tactic:
dsimp
-- 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
D1 D2 : LieDerivation R L L
⊢ (↑⁅D1, D2⁆ : L →ₗ[R] L) = ⁅(↑D1 : L →ₗ[R] L), (↑D2 : L →ₗ[R] L)⁆

Tactic:
dsimp
-- 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
⊢ Function.Injective (α := LieDerivation R L L) (β := L →ₗ[R] L)
    (⇑(toLinearMapLieHom R L) : (a : LieDerivation R L L) → L →ₗ[R] L)

Tactic:
fun _ _ h ↦ ext fun a ↦ congrFun (congrArg DFunLike.coe h) a

Premises used: congrArg, LieDerivation.ext, congrFun, Function.Injective, 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
inst_3 : IsNoetherian R L
⊢ IsNoetherian.{u_1, u_2} R (LieDerivation R L L)

Tactic:
isNoetherian_of_linearEquiv (LinearEquiv.ofInjective _ (toLinearMapLieHom_injective R L)).symm

Premises used: LinearEquiv.symm, LieDerivation.toLinearMapLieHom_injective, LinearEquiv.ofInjective, isNoetherian_of_linearEquiv
-- 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
m : M
⊢ ∀ (a b : L),
    (((LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m : L →ₗ[R] M) :
          (a : L) → M)
        ⁅a, b⁆ =
      HSub.hSub (α := M) (β := M)
        (⁅a,
            (((LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m :
                  L →ₗ[R] M) :
                (a : L) → M)
              b⁆ :
          M)
        (⁅b,
            (((LinearMap.flip (↑(LieModule.toEnd R L M) : L →ₗ[R] Module.End R M) : (a : M) → L →ₗ[R] M) m :
                  L →ₗ[R] M) :
                (a : L) → M)
              a⁆ :
          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
m n : M
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' := ⋯ } :
            (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' := ⋯ : 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 }) :
            (a : L) → M)
          a :
        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 })

Tactic:
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
m n : M
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' := ⋯ } :
          (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' := ⋯ : 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 }) :
          (a : L) → M)
        a :
      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
t : R
m : M
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' := ⋯ } :
            (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' := ⋯ : LieDerivation R L M }) :
            (a : L) → M)
          a :
        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 })

Tactic:
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
t : R
m : M
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' := ⋯ } :
          (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' := ⋯ : LieDerivation R L M }) :
          (a : L) → M)
        a :
      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
x y : L
D : LieDerivation R L M
⊢ (inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) (x + y) : M) =
    HAdd.hAdd (α := LieDerivation R L M) (β := LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) x : M) : LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) y : M) : LieDerivation R L 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
x : L
D₁ D₂ : LieDerivation R L M
⊢ (inner R L M : (a : M) → LieDerivation R L M) ((D₁ + D₂ : (a : L) → M) x : M) =
    HAdd.hAdd (α := LieDerivation R L M) (β := LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M) ((D₁ : (a : L) → M) x : M) : LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M) ((D₂ : (a : L) → M) x : M) : LieDerivation R L 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
x y : L
D : LieDerivation R L M
⊢ (inner R L M : (a : M) → LieDerivation R L M)
      ((((inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) y : M) : LieDerivation R L M) : (a : L) → M)
          x :
        M) =
    HAdd.hAdd (α := LieDerivation R L M) (β := LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) ⁅x, y⁆ : M) : LieDerivation R L M)
      ((inner R L M : (a : M) → LieDerivation R L M)
          ((((inner R L M : (a : M) → LieDerivation R L M) ((D : (a : L) → M) x : M) : LieDerivation R L M) :
                (a : L) → M)
              y :
            M) :
        LieDerivation R L 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
x y : L
D : LieDerivation R L M
⊢ Eq.{u_3 + 1} (α := M) ((⁅x, D⁆ : (a : L) → M) y : M) (⁅y, (D : (a : L) → M) x⁆ : 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
x : L
D : LieDerivation R L M
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)
⊢ ⁅x, (↑D : L →ₗ[R] M)⁆ = (↑⁅x, D⁆ : L →ₗ[R] M)

Tactic:
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
x : L
D : LieDerivation R L M
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:
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
t : R
x : L
D : LieDerivation R L M
H : ∀ (a : L), Eq.{u_3 + 1} (α := M) ((⁅t • x, D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : M)
⊢ ⁅t • x, D⁆ = t • ⁅x, D⁆

Tactic:
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
t : R
x : L
D : LieDerivation R L M
a : L
⊢ Eq.{u_3 + 1} (α := M) ((⁅t • x, D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : 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
t : R
x : L
D : LieDerivation R L M
H : ∀ (a : L), Eq.{u_3 + 1} (α := M) ((⁅x, t • D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : M)
⊢ ⁅x, t • D⁆ = t • ⁅x, D⁆

Tactic:
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
t : R
x : L
D : LieDerivation R L M
a : L
⊢ Eq.{u_3 + 1} (α := M) ((⁅x, t • D⁆ : (a : L) → M) a : M) ((t • ⁅x, D⁆ : (a : L) → M) a : M)

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
x : L
D₁ D₂ : LieDerivation R L L
H : ∀ (y : L), Eq (α := L) ((⁅x, ⁅D₁, D₂⁆⁆ : (a : L) → L) y : L) ((⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ : (a : L) → L) y : L)
⊢ ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Tactic:
ext y
-- 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
x : L
D₁ D₂ : LieDerivation R L L
y : L
⊢ Eq (α := L) ((⁅x, ⁅D₁, D₂⁆⁆ : (a : L) → L) y : L) ((⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ : (a : L) → L) y : L)

Tactic:
simp [-lie_skew, ← lie_skew (D₁ x) (D₂ y), ← lie_skew (D₂ x) (D₁ y), sub_eq_neg_add]

Premises used: sub_eq_neg_add, lie_skew, 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
⊢ SMulCommClass R L L

Tactic:
have : SMulCommClass R L L := LieAlgebra.smulCommClass R L
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
this : SMulCommClass R L L
⊢ IsScalarTower R L L

Tactic:
have : IsScalarTower R L L := LieAlgebra.isScalarTower R L
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
this_1 : SMulCommClass R L L
this : IsScalarTower R L 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⁆

Tactic:
Module.End.exp_mul_of_derivation R L D.toLinearMap D.apply_lie_eq_add h

Premises used: Module.End.exp_mul_of_derivation, LieDerivation.apply_lie_eq_add, LieDerivation.toLinearMap
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
this_1 : SMulCommClass R L L
this : IsScalarTower R L 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⁆

Tactic:
exact Module.End.exp_mul_of_derivation R L D.toLinearMap D.apply_lie_eq_add h

Premises used: Module.End.exp_mul_of_derivation, LieDerivation.apply_lie_eq_add, LieDerivation.toLinearMap
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
x : L
⊢ (fun (x : L) ↦ ((IsNilpotent.exp (-(↑D : L →ₗ[R] L)) : (a : L) → L) x : L))
      ((IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun x) =
    x

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply,
        ← Module.End.mul_eq_comp, h.exp_neg_mul_exp_self, Module.End.one_apply]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_apply, AddHom.toFun_eq_coe, Module.End.one_apply, IsNilpotent.exp_neg_mul_exp_self, LinearMap.coe_toAddHom
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
x : L
⊢ (IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun
      ((fun (x : L) ↦ ((IsNilpotent.exp (-(↑D : L →ₗ[R] L)) : (a : L) → L) x : L)) x) =
    x

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply,
        ← Module.End.mul_eq_comp, h.exp_mul_exp_neg_self, Module.End.one_apply]

Premises used: IsNilpotent.exp_mul_exp_neg_self, Module.End.mul_eq_comp, LinearMap.comp_apply, AddHom.toFun_eq_coe, Module.End.one_apply, LinearMap.coe_toAddHom
-- 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
⊢ (↑(D.exp h).toLinearEquiv : L →ₗ[R] L) = IsNilpotent.exp (↑D : L →ₗ[R] L)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, IsNilpotent.exp, Finset.sum, 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
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
l : L
⊢ Eq (α := L) ((D.exp h : (a : L) → L) l : L) ((IsNilpotent.exp (↑D : L →ₗ[R] L) : (a : L) → L) l : L)

Tactic:
DFunLike.congr_fun (exp_apply D h) l

Premises used: DFunLike.congr_fun, LieDerivation.exp_apply
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
rw :
  Eq (α :=
    LinearMap.BilinForm.{u_1, u_2} R
      ↥(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    (killingForm R ↥(LieHom.idealRange (ad R L)) : LinearMap.BilinForm.{u_1, u_2} R ↥(LieHom.idealRange (ad R L)))
    (killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L))))
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (killingForm R ↥(LieHom.range (ad R L)))

Tactic:
rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]

Premises used: LieHom.IsIdealMorphism.eq, LieDerivation.ad_isIdealMorphism, LieIdeal.killingForm_eq
-- Module: Mathlib.Algebra.Lie.Derivation.Killing
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
⊢ Eq (α :=
    LinearMap.BilinForm.{u_1, u_2} R
      ↥(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    (killingForm R ↥(LieHom.idealRange (ad R L)) : LinearMap.BilinForm.{u_1, u_2} R ↥(LieHom.idealRange (ad R L)))
    (killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L))))

Tactic:
rfl