R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a = -(a ^ 2 • ↑D b)
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a = -a ^ 2 • ↑D b
rw [neg_smul]
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a + a ^ 2 • ↑D b = 0
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a = -(a ^ 2 • ↑D b)
refine' eq_neg_of_add_eq_zero_left _
no goals
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a + a ^ 2 • ↑D b = 0
calc
  D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
  _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
  _ = 0 := by rw [h, map_one_eq_zero, smul_zero]
no goals
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a + a ^ 2 • ↑D b = a • b • ↑D a + a • a • ↑D b
simp only [smul_smul, h, one_smul, sq]
no goals
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ a • b • ↑D a + a • a • ↑D b = a • ↑D (a * b)
rw [leibniz, smul_add, add_comm]
no goals
R : Type u_3
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ a • ↑D (a * b) = 0
rw [h, map_one_eq_zero, smul_zero]