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)
      (⁅((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)
        (⁅((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)
        (⁅((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:
by
    rw [← of_add]
    refine Equiv.congr_arg ?_
    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]
    have hc := c.2
    rw [mem_twoCocycle_iff] at hc
    have := d₂₃_apply R L M c ((ofProd c).symm x).1 ((ofProd c).symm y).1 ((ofProd c).symm z).1
    simp only [hc, LinearMap.zero_apply] at this
    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
    rw [this]
    abel

Goal state after: