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
⊢ Eq (α := L →ₗ[R] M) (↑0 : L →ₗ[R] M) 0

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
a : L
⊢ Eq.{u_3 + 1} (α := M) ((0 : (a : L) → M) a : M) (0 : 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
D D1_1 D2_1 : LieDerivation R L M
a_1 b_1 : L
D1 D2 : LieDerivation R L M
a b : L
⊢ ((↑D1 : L →ₗ[R] M) + (↑D2 : L →ₗ[R] M) : (a : L) → M) ⁅a, b⁆ =
    HSub.hSub (α := M) (β := M) (⁅a, ((↑D1 : L →ₗ[R] M) + (↑D2 : L →ₗ[R] M) : (a : L) → M) b⁆ : M)
      (⁅b, ((↑D1 : L →ₗ[R] M) + (↑D2 : L →ₗ[R] M) : (a : L) → M) a⁆ : M)

Tactic:
simp only [LinearMap.add_apply, coeFn_coe, apply_lie_eq_sub, lie_add, add_sub_add_comm]

Premises used: LinearMap.add_apply, add_sub_add_comm, LieDerivation.apply_lie_eq_sub, LieDerivation.coeFn_coe, lie_add
-- 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
⊢ (⇑(D1 + D2) : (a : L) → M) = HAdd.hAdd (α := (a : L) → M) (⇑D1 : (a : L) → M) (⇑D2 : (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
D1 D2 : LieDerivation R L M
⊢ (↑(D1 + D2) : L →ₗ[R] M) = (↑D1 : L →ₗ[R] M) + (↑D2 : L →ₗ[R] 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
D1 D2 : LieDerivation R L M
a : L
⊢ (D1 + D2 : (a : L) → M) a = HAdd.hAdd (α := M) (β := M) ((D1 : (a : L) → M) a : M) ((D2 : (a : L) → M) a : 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
D : LieDerivation R L M
a : L
⊢ Eq.{u_3 + 1} (α := M) ((D : (a : L) → M) (-a) : M) (-(D : (a : L) → M) a : M)

Tactic:
map_neg D a

Premises used: map_neg
-- 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) ((D : (a : L) → M) a : M) ((D : (a : L) → M) b : M)

Tactic:
map_sub D a b

Premises used: map_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
D_1 D1 D2 : LieDerivation R L M
a_1 b_1 : L
D : LieDerivation R L M
a b : L
⊢ (-(↑D : L →ₗ[R] M) : (a : L) → M) ⁅a, b⁆ =
    HSub.hSub (α := M) (β := M) (⁅a, (-(↑D : L →ₗ[R] M) : (a : L) → M) b⁆ : M)
      (⁅b, (-(↑D : L →ₗ[R] M) : (a : L) → M) a⁆ : M)

Tactic:
simp only [LinearMap.neg_apply, coeFn_coe, apply_lie_eq_sub,
        neg_sub, lie_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]

Premises used: neg_sub, lie_neg, sub_eq_add_neg, LinearMap.neg_apply, add_comm, LieDerivation.apply_lie_eq_sub, LieDerivation.coeFn_coe, sub_neg_eq_add
-- 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
⊢ Eq (α := (a : L) → M) (⇑(-D) : (a : L) → M) (-(⇑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
D : LieDerivation R L M
⊢ (↑(-D) : L →ₗ[R] M) = -(↑D : L →ₗ[R] 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
D : LieDerivation R L M
a : L
⊢ Eq.{u_3 + 1} (α := M) ((-D : (a : L) → M) a : M) (-(D : (a : L) → M) a : 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
D D1_1 D2_1 : LieDerivation R L M
a_1 b_1 : L
D1 D2 : LieDerivation R L M
a b : L
⊢ ((↑D1 : L →ₗ[R] M) - (↑D2 : L →ₗ[R] M) : (a : L) → M) ⁅a, b⁆ =
    HSub.hSub (α := M) (β := M) (⁅a, ((↑D1 : L →ₗ[R] M) - (↑D2 : L →ₗ[R] M) : (a : L) → M) b⁆ : M)
      (⁅b, ((↑D1 : L →ₗ[R] M) - (↑D2 : L →ₗ[R] M) : (a : L) → M) a⁆ : M)

Tactic:
simp only [LinearMap.sub_apply, coeFn_coe, apply_lie_eq_sub, lie_sub, sub_sub_sub_comm]

Premises used: sub_sub_sub_comm, lie_sub, LinearMap.sub_apply, LieDerivation.apply_lie_eq_sub, LieDerivation.coeFn_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
D1 D2 : LieDerivation R L M
⊢ (⇑(D1 - D2) : (a : L) → M) = HSub.hSub (α := (a : L) → M) (⇑D1 : (a : L) → M) (⇑D2 : (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
D1 D2 : LieDerivation R L M
⊢ (↑(D1 - D2) : L →ₗ[R] M) = (↑D1 : L →ₗ[R] M) - (↑D2 : L →ₗ[R] 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
a : L
D1 D2 : LieDerivation R L M
⊢ (D1 - D2 : (a : L) → M) a = HSub.hSub (α := M) (β := M) ((D1 : (a : L) → M) a : M) ((D2 : (a : L) → M) a : 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
D_1 D1 D2 : LieDerivation R L M
a_1 b_1 : L
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
r : S
D : LieDerivation R L M
a b : L
⊢ (r • (↑D : L →ₗ[R] M) : (a : L) → M) ⁅a, b⁆ =
    HSub.hSub (α := M) (β := M) (⁅a, (r • (↑D : L →ₗ[R] M) : (a : L) → M) b⁆ : M)
      (⁅b, (r • (↑D : L →ₗ[R] M) : (a : L) → M) a⁆ : M)

Tactic:
simp only [LinearMap.smul_apply, coeFn_coe, apply_lie_eq_sub,
        smul_sub, SMulBracketCommClass.smul_bracket_comm]

Premises used: LinearMap.smul_apply, smul_sub, LieDerivation.SMulBracketCommClass.smul_bracket_comm, LieDerivation.apply_lie_eq_sub, LieDerivation.coeFn_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
S : Type u_4
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
r : S
D : LieDerivation R L M
⊢ (⇑(r • D) : (a : L) → M) = HSMul.hSMul (β := (a : L) → M) r (⇑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
S : Type u_4
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
r : S
D : LieDerivation R L M
⊢ (↑(r • D) : L →ₗ[R] M) = r • (↑D : L →ₗ[R] 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
a : L
S : Type u_4
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
r : S
D : LieDerivation R L M
⊢ (r • D : (a : L) → M) a = HSMul.hSMul (β := M) r ((D : (a : L) → M) a : 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
D D1 D2 : LieDerivation R L M
a b : L
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
⊢ SMulBracketCommClass R L M

Tactic:
⟨fun s l a ↦ (lie_smul s l a).symm⟩

Premises used: lie_smul, LieDerivation.SMulBracketCommClass.mk, Eq.symm
-- 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
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
⊢ SMulBracketCommClass ℕ L M

Tactic:
⟨fun s l a => (lie_nsmul l a s).symm⟩

Premises used: LieDerivation.SMulBracketCommClass.mk, lie_nsmul, Eq.symm
-- 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
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
⊢ SMulBracketCommClass ℤ L M

Tactic:
⟨fun s l a => (lie_zsmul l a s).symm⟩

Premises used: LieDerivation.SMulBracketCommClass.mk, lie_zsmul, Eq.symm
-- 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
⊢ Eq (α := L → M) ((coeFnAddMonoidHom : (a : LieDerivation R L M) → L → M) D : L → M) ((⇑D : (a : L) → M) : (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
D D1 D2 : LieDerivation R L M
a b : L
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
inst_15 : SMul S T
inst_16 : IsScalarTower S T M
⊢ IsScalarTower S T (LieDerivation R L M)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Premises used: smul_assoc, LieDerivation.ext, LieDerivation.toLinearMap, IsScalarTower.mk, 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 b : L
S : Type u_4
T : Type u_5
inst_7 : Monoid S
inst_8 : DistribMulAction S M
inst_9 : SMulCommClass R S M
inst_10 : SMulBracketCommClass S L M
inst_11 : Monoid T
inst_12 : DistribMulAction T M
inst_13 : SMulCommClass R T M
inst_14 : SMulBracketCommClass T L M
inst_15 : SMulCommClass S T M
⊢ SMulCommClass S T (LieDerivation R L M)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Premises used: LieDerivation.ext, LieDerivation.toLinearMap, SMulCommClass.smul_comm, SMulCommClass.mk, 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
D1 D2 : LieDerivation R L L
a b : L
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)
⊢ (⁅(↑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)

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]

Premises used: LieDerivation.apply_lie_eq_add, map_add, lie_skew, lie_sub, Ring.lie_def, LinearMap.sub_apply, Module.End.mul_apply, LieDerivation.coeFn_coe, sub_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
D1 D2 : LieDerivation R L L
a b : L
⊢ 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:
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
⊢ (↑⁅D1, D2⁆ : L →ₗ[R] L) = ⁅(↑D1 : L →ₗ[R] L), (↑D2 : L →ₗ[R] 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
a : L
⊢ (⁅D1, D2⁆ : (a : L) → L) a =
    HSub.hSub (α := L) (β := L) ((D1 : (a : L) → L) ((D2 : (a : L) → L) a : L) : L)
      ((D2 : (a : L) → L) ((D1 : (a : L) → L) a : 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 d e f : LieDerivation R L L
H : ∀ (a : L), Eq (α := L) ((⁅d + e, f⁆ : (a : L) → L) a : L) ((⁅d, f⁆ + ⁅e, f⁆ : (a : L) → L) a : L)
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

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 d e f : LieDerivation R L L
a : L
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)
⊢ Eq (α := L) ((⁅d + e, f⁆ : (a : L) → L) a : L) ((⁅d, f⁆ + ⁅e, f⁆ : (a : L) → L) a : L)

Tactic:
simp only [commutator_apply, add_apply, map_add]

Premises used: LieDerivation.commutator_apply, map_add, 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
⊢ 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:
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 d e f : LieDerivation R L L
H : ∀ (a : L), Eq (α := L) ((⁅d, e + f⁆ : (a : L) → L) a : L) ((⁅d, e⁆ + ⁅d, f⁆ : (a : L) → L) a : L)
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

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 d e f : LieDerivation R L L
a : L
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)
⊢ Eq (α := L) ((⁅d, e + f⁆ : (a : L) → L) a : L) ((⁅d, e⁆ + ⁅d, f⁆ : (a : L) → L) a : L)

Tactic:
simp only [commutator_apply, add_apply, map_add]

Premises used: LieDerivation.commutator_apply, map_add, 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
⊢ 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:
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 d : LieDerivation R L L
H : ∀ (a : L), Eq (α := L) ((⁅d, d⁆ : (a : L) → L) a : L) ((0 : (a : L) → L) a : L)
⊢ ⁅d, d⁆ = 0

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 d : LieDerivation R L L
a : L
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
⊢ Eq (α := L) ((⁅d, d⁆ : (a : L) → L) a : L) ((0 : (a : L) → L) a : L)

Tactic:
simp only [commutator_apply, zero_apply]

Premises used: LieDerivation.zero_apply, LieDerivation.commutator_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 : LieDerivation R L L
a : L
⊢ 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:
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 d e f : LieDerivation R L L
H : ∀ (a : L), Eq (α := L) ((⁅d, ⁅e, f⁆⁆ : (a : L) → L) a : L) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : L) → L) a : L)
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
ext a