∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) (M : Type u_5) (N : Type u_3) (P : Type u_4) [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P] [inst_13 : LieRingModule L P]
  [inst_14 : LieModule R L P], LieModule R L (M →ₗ[R] N →ₗ[R] P)