∀ (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]
  (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x : L) (x_1 : R) (x_2 x_3 x_4 : L),
  ⁅x, (a (x_1 • x_2)) (x_3 + x_4)⁆ - ⁅x_1 • x_2, (a x) (x_3 + x_4)⁆ + ⁅x_3 + x_4, (a x) (x_1 • x_2)⁆ -
          (a ⁅x, x_1 • x_2⁆) (x_3 + x_4) +
        (a ⁅x, x_3 + x_4⁆) (x_1 • x_2) -
      (a ⁅x_1 • x_2, x_3 + x_4⁆) x =
    ⁅x, (a (x_1 • x_2)) x_3⁆ - ⁅x_1 • x_2, (a x) x_3⁆ + ⁅x_3, (a x) (x_1 • x_2)⁆ - (a ⁅x, x_1 • x_2⁆) x_3 +
          (a ⁅x, x_3⁆) (x_1 • x_2) -
        (a ⁅x_1 • x_2, x_3⁆) x +
      (⁅x, (a (x_1 • x_2)) x_4⁆ - ⁅x_1 • x_2, (a x) x_4⁆ + ⁅x_4, (a x) (x_1 • x_2)⁆ - (a ⁅x, x_1 • x_2⁆) x_4 +
          (a ⁅x, x_4⁆) (x_1 • x_2) -
        (a ⁅x_1 • x_2, x_4⁆) x)