[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1✝ D2✝ : Derivation R A A
a✝ : A
D1 D2 : Derivation R A A
a b : A
⊢ ↑⁅↑D1, ↑D2⁆ (a * b) = a • ↑⁅↑D1, ↑D2⁆ b + b • ↑⁅↑D1, ↑D2⁆ a
[PROOFSTEP]
simp only [Ring.lie_def, map_add, Algebra.id.smul_eq_mul, LinearMap.mul_apply, leibniz, coeFn_coe, LinearMap.sub_apply]
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1✝ D2✝ : Derivation R A A
a✝ : A
D1 D2 : Derivation R A A
a b : A
⊢ a * ↑D1 (↑D2 b) + ↑D2 b * ↑D1 a + (b * ↑D1 (↑D2 a) + ↑D2 a * ↑D1 b) -
      (a * ↑D2 (↑D1 b) + ↑D1 b * ↑D2 a + (b * ↑D2 (↑D1 a) + ↑D1 a * ↑D2 b)) =
    a * (↑D1 (↑D2 b) - ↑D2 (↑D1 b)) + b * (↑D1 (↑D2 a) - ↑D2 (↑D1 a))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑⁅d + e, f⁆ a = ↑(⁅d, f⁆ + ⁅e, f⁆) a
[PROOFSTEP]
simp only [commutator_apply, add_apply, map_add]
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑d (↑f a) + ↑e (↑f a) - (↑f (↑d a) + ↑f (↑e a)) = ↑d (↑f a) - ↑f (↑d a) + (↑e (↑f a) - ↑f (↑e a))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑⁅d, e + f⁆ a = ↑(⁅d, e⁆ + ⁅d, f⁆) a
[PROOFSTEP]
simp only [commutator_apply, add_apply, map_add]
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑d (↑e a) + ↑d (↑f a) - (↑e (↑d a) + ↑f (↑d a)) = ↑d (↑e a) - ↑e (↑d a) + (↑d (↑f a) - ↑f (↑d a))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a : A
d : Derivation R A A
⊢ ⁅d, d⁆ = 0
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ ↑⁅d, d⁆ a = ↑0 a
[PROOFSTEP]
simp only [commutator_apply, add_apply, map_add]
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ ↑d (↑d a) - ↑d (↑d a) = ↑0 a
[PROOFSTEP]
ring_nf
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ 0 = ↑0 a
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑⁅d, ⁅e, f⁆⁆ a = ↑(⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a
[PROOFSTEP]
simp only [commutator_apply, add_apply, sub_apply, map_sub]
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ↑d (↑e (↑f a)) - ↑d (↑f (↑e a)) - (↑e (↑f (↑d a)) - ↑f (↑e (↑d a))) =
    ↑d (↑e (↑f a)) - ↑e (↑d (↑f a)) - (↑f (↑d (↑e a)) - ↑f (↑e (↑d a))) +
      (↑e (↑d (↑f a)) - ↑e (↑f (↑d a)) - (↑d (↑f (↑e a)) - ↑f (↑d (↑e a))))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a : A
src✝ : Module R (Derivation R A A) := instModule
r : R
d e : Derivation R A A
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D D1 D2 : Derivation R A A
a✝ : A
src✝ : Module R (Derivation R A A) := instModule
r : R
d e : Derivation R A A
a : A
⊢ ↑⁅d, r • e⁆ a = ↑(r • ⁅d, e⁆) a
[PROOFSTEP]
simp only [commutator_apply, map_smul, smul_sub, smul_apply]
