∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : AddCommMonoid M] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Module A M] [inst_7 : Module B M] [inst_8 : Module R M] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower A B M] [inst_12 : IsScalarTower R B M] (d : Derivation R B M)
  (a : A), ((Derivation.compAlgebraMapL R A B M) d) a = d ((algebraMap A B) a)