Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝⁴ x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ (({
            toFun := fun x ↦
              {
                toFun := fun y ↦
                  {
                    toFun := fun z ↦
                      ⁅x, ((x✝⁴ + x✝³) y) z⁆ - ⁅y, ((x✝⁴ + x✝³) x) z⁆ + ⁅z, ((x✝⁴ + x✝³) x) y⁆ -
                            ((x✝⁴ + x✝³) ⁅x, y⁆) z +
                          ((x✝⁴ + x✝³) ⁅x, z⁆) y -
                        ((x✝⁴ + x✝³) ⁅y, z⁆) x,
                    map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          x✝²)
        x✝¹)
      x✝ =
    ((({
              toFun := fun x ↦
                {
                  toFun := fun y ↦
                    {
                      toFun := fun z ↦
                        ⁅x, (x✝⁴ y) z⁆ - ⁅y, (x✝⁴ x) z⁆ + ⁅z, (x✝⁴ x) y⁆ - (x✝⁴ ⁅x, y⁆) z + (x✝⁴ ⁅x, z⁆) y -
                          (x✝⁴ ⁅y, z⁆) x,
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } +
            {
              toFun := fun x ↦
                {
                  toFun := fun y ↦
                    {
                      toFun := fun z ↦
                        ⁅x, (x✝³ y) z⁆ - ⁅y, (x✝³ x) z⁆ + ⁅z, (x✝³ x) y⁆ - (x✝³ ⁅x, y⁆) z + (x✝³ ⁅x, z⁆) y -
                          (x✝³ ⁅y, z⁆) x,
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ })
          x✝²)
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝⁴ x✝³ : ↥(twoCochain R L M)
x✝² x✝¹ x✝ : L
⊢ (({
            toFun := fun x ↦
              {
                toFun := fun y ↦
                  {
                    toFun := fun z ↦
                      ⁅x, ((x✝⁴ + x✝³) y) z⁆ - ⁅y, ((x✝⁴ + x✝³) x) z⁆ + ⁅z, ((x✝⁴ + x✝³) x) y⁆ -
                            ((x✝⁴ + x✝³) ⁅x, y⁆) z +
                          ((x✝⁴ + x✝³) ⁅x, z⁆) y -
                        ((x✝⁴ + x✝³) ⁅y, z⁆) x,
                    map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          x✝²)
        x✝¹)
      x✝ =
    ((({
              toFun := fun x ↦
                {
                  toFun := fun y ↦
                    {
                      toFun := fun z ↦
                        ⁅x, (x✝⁴ y) z⁆ - ⁅y, (x✝⁴ x) z⁆ + ⁅z, (x✝⁴ x) y⁆ - (x✝⁴ ⁅x, y⁆) z + (x✝⁴ ⁅x, z⁆) y -
                          (x✝⁴ ⁅y, z⁆) x,
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } +
            {
              toFun := fun x ↦
                {
                  toFun := fun y ↦
                    {
                      toFun := fun z ↦
                        ⁅x, (x✝³ y) z⁆ - ⁅y, (x✝³ x) z⁆ + ⁅z, (x✝³ x) y⁆ - (x✝³ ⁅x, y⁆) z + (x✝³ ⁅x, z⁆) y -
                          (x✝³ ⁅y, z⁆) x,
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ })
          x✝²)
        x✝¹)
      x✝