Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
hc : (d₂₃ R L M) ↑c = 0
this :
  0 =
    ⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ -
              ⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ -
          (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
        (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆) ((ofProd c).symm y).1 -
      (↑c ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆) ((ofProd c).symm x).1
⊢ (↑c ((ofProd c).symm x).1) ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆ +
        (⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
          ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆) -
      (⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆ -
        ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) =
    (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
          (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆) -
        (⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ +
            ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) +
      ((↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆ +
          (⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
              ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆) -
        (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆))

Tactic:
rw [← twoCochain_skew _ _ ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
      ← twoCochain_skew _ _ ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆, eq_sub_iff_add_eq,
      zero_add, neg_eq_iff_eq_neg] at this

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
hc : (d₂₃ R L M) ↑c = 0
this :
  (↑c ((ofProd c).symm x).1) ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆ =
    -(⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ -
              ⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ -
          (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
        -(↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆)
⊢ (↑c ((ofProd c).symm x).1) ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆ +
        (⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
          ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆) -
      (⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆ -
        ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) =
    (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
          (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆) -
        (⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ +
            ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) +
      ((↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆ +
          (⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
              ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆) -
        (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆))