(R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → LieAlgebra A (TensorProduct R A L)