-- 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
x x_1 : ↥(twoCochain R L M)
x_2 x_3 x_4 : L
h :
  HAdd.hAdd (α := M) (β := M) (⁅x_2, (((x : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅x_3, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_4, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M)
            ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M) +
        HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
          ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) -
      HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
        ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) =
    HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x_2, (((x : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M))
              (⁅x_4, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M))
          ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((x : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M)
                (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M))
              (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M))
          ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
⊢ Eq.{u_3 + 1} (α := M)
    ((((((d₂₃_aux R L M (x + x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_3 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_4 :
      M)
    ((((((d₂₃_aux R L M x + d₂₃_aux R L M x_1 : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x_3 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_4 :
      M)

Tactic:
simp [d₂₃_aux]

Premises used: _private.0.LieModule.Cohomology.d₂₃_aux