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
⊢ (⁅((ofProd c).symm x).1,
        ((ofProd c).symm
            ((ofProd c)
              (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
                (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
                  ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))).1⁆,
      (↑↑c ((ofProd c).symm x).1)
            ((ofProd c).symm
                ((ofProd c)
                  (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
                    (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
                      ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))).1 +
          ⁅((ofProd c).symm x).1,
            ((ofProd c).symm
                ((ofProd c)
                  (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
                    (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
                      ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))).2⁆ -
        ⁅((ofProd c).symm
              ((ofProd c)
                (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
                  (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
                    ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))).1,
          ((ofProd c).symm x).2⁆) =
    (⁅((ofProd c).symm
              ((ofProd 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 x).1, ((ofProd c).symm y).2⁆ -
                    ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆))).1,
          ((ofProd c).symm z).1⁆,
        (↑↑c
                ((ofProd c).symm
                    ((ofProd 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 x).1, ((ofProd c).symm y).2⁆ -
                          ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆))).1)
              ((ofProd c).symm z).1 +
            ⁅((ofProd c).symm
                  ((ofProd 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 x).1, ((ofProd c).symm y).2⁆ -
                        ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆))).1,
              ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1,
            ((ofProd c).symm
                ((ofProd 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 x).1, ((ofProd c).symm y).2⁆ -
                      ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆))).2⁆) +
      (⁅((ofProd c).symm y).1,
          ((ofProd c).symm
              ((ofProd c)
                (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
                  (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
                    ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆))).1⁆,
        (↑↑c ((ofProd c).symm y).1)
              ((ofProd c).symm
                  ((ofProd c)
                    (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
                      (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 +
                          ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
                        ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆))).1 +
            ⁅((ofProd c).symm y).1,
              ((ofProd c).symm
                  ((ofProd c)
                    (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
                      (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 +
                          ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
                        ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆))).2⁆ -
          ⁅((ofProd c).symm
                ((ofProd c)
                  (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
                    (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
                      ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆))).1,
            ((ofProd c).symm y).2⁆)

Tactic:
simp only [twoCochain_val_apply, Equiv.symm_apply_apply, lie_lie, Prod.mk_add_mk,
      sub_add_cancel, Prod.mk.injEq, true_and, lie_add, lie_sub]

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
⊢ (↑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⁆⁆))