-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (goal)
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 x_1 x_2 x_3 : L
⊢ Eq.{u_3 + 1} (α := M)
    (((({
                  toFun := fun (y : L) ↦
                    {
                      toFun := fun (z : L) ↦
                        HSub.hSub (β := M)
                          (HAdd.hAdd (β := M)
                            (HSub.hSub (β := M)
                              (HAdd.hAdd (β := M)
                                (HSub.hSub (α := M) (β := M)
                                  (⁅x + x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                                  (⁅y, (((a : (a : L) → L →ₗ[R] M) (x + x_1) : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                                (⁅z, (((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_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                            ((((a : (a : L) → L →ₗ[R] M) ⁅x + x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                          ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) (x + x_1) : M),
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ } :
                (a : L) → L →ₗ[R] M)
              x_2 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_3 :
      M)
    ((((HAdd.hAdd (α := L →ₗ[R] L →ₗ[R] M)
                  {
                    toFun := fun (y : L) ↦
                      {
                        toFun := fun (z : L) ↦
                          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) z⁆ : M)
                                    (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                                  (⁅z, (((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) z : M))
                              ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                            ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
                        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
                    map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }
                  {
                    toFun := fun (y : L) ↦
                      {
                        toFun := fun (z : L) ↦
                          HSub.hSub (β := M)
                            (HAdd.hAdd (β := M)
                              (HSub.hSub (β := M)
                                (HAdd.hAdd (β := M)
                                  (HSub.hSub (α := M) (β := M)
                                    (⁅x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                                    (⁅y, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                                  (⁅z, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
                                ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                              ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                            ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M),
                        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
                    map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M } :
                (a : L) → L →ₗ[R] M)
              x_2 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_3 :
      M)
have h : HAdd.hAdd (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
            HAdd.hAdd (α := M) (β := M) (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) +
          HAdd.hAdd (α := M) (β := M) (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
            (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) -
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
          ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) +
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) -
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
      ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M) =
  HSub.hSub (β := M)
      (HAdd.hAdd (β := M)
        (HSub.hSub (β := M)
          (HAdd.hAdd (β := M)
            (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : 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_1, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)
Tactic: simp