∀ (R : Type u_3) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_1)
  [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 x_1 x_2 x_3 : L),
  {
      toFun := fun z =>
        ⁅x + x_1, (a (x_2 + x_3)) z⁆ - ⁅x_2 + x_3, (a (x + x_1)) z⁆ + ⁅z, (a (x + x_1)) (x_2 + x_3)⁆ -
              (a ⁅x + x_1, x_2 + x_3⁆) z +
            (a ⁅x + x_1, z⁆) (x_2 + x_3) -
          (a ⁅x_2 + x_3, z⁆) (x + x_1),
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun z =>
          ⁅x + x_1, (a x_2) z⁆ - ⁅x_2, (a (x + x_1)) z⁆ + ⁅z, (a (x + x_1)) x_2⁆ - (a ⁅x + x_1, x_2⁆) z +
              (a ⁅x + x_1, z⁆) x_2 -
            (a ⁅x_2, z⁆) (x + x_1),
        map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun z =>
          ⁅x + x_1, (a x_3) z⁆ - ⁅x_3, (a (x + x_1)) z⁆ + ⁅z, (a (x + x_1)) x_3⁆ - (a ⁅x + x_1, x_3⁆) z +
              (a ⁅x + x_1, z⁆) x_3 -
            (a ⁅x_3, z⁆) (x + x_1),
        map_add' := ⋯, map_smul' := ⋯ }