no goals
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
⊢ ↑D (↑(algebraMap R A) r) = 0
rw [← mul_one r, RingHom.map_mul, RingHom.map_one, ← smul_def, map_smul, map_one_eq_zero,
  smul_zero]