-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
a : ↥(twoCochain R L M)
x y x_1 x_2 : L
simp :
  HAdd.hAdd (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M)
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) +
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) y : M)
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M) -
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M))
              (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
⊢ HSub.hSub (β := M)
      (HAdd.hAdd (β := M)
        (HSub.hSub (β := M)
          (HAdd.hAdd (β := M)
            (HSub.hSub (α := M) (β := M)
              (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2)⁆ : M)
              (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2)⁆ : M))
            (⁅x_1 + x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2) : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1 + x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1 + x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M))
              (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M)

Tactic:
simp