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:
← of_add

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