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)
⊢ {
      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' := ⋯ } =
    {
        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' := ⋯ }

Tactic:
ext

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✝