∀ (R : Type u_3) [inst : CommRing R] (L : Type u_1) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_2)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x : R) (x_1 : L),
  {
      toFun := fun y =>
        {
          toFun := fun z =>
            ⁅x • x_1, (a y) z⁆ - ⁅y, (a (x • x_1)) z⁆ + ⁅z, (a (x • x_1)) y⁆ - (a ⁅x • x_1, y⁆) z + (a ⁅x • x_1, z⁆) y -
              (a ⁅y, z⁆) (x • x_1),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x •
      {
        toFun := fun y =>
          {
            toFun := fun z =>
              ⁅x_1, (a y) z⁆ - ⁅y, (a x_1) z⁆ + ⁅z, (a x_1) y⁆ - (a ⁅x_1, y⁆) z + (a ⁅x_1, z⁆) y - (a ⁅y, z⁆) x_1,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }