-- 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 : oneCochain R L M
x y z : L
this_1 :
  ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
this :
  (a : (a : L) → M) ⁅y, ⁅z, x⁆⁆ =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
⊢ HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M))
                (⁅x, (a : (a : L) → M) ⁅y, z⁆⁆ : M) -
              HSub.hSub (β := M)
                (HSub.hSub (β := M)
                  (HAdd.hAdd (α := M) (β := M) (⁅⁅y, x⁆, (a : (a : L) → M) z⁆ : M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M))
                  (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
                (⁅y, (a : (a : L) → M) ⁅x, z⁆⁆ : M) +
            HSub.hSub (β := M)
              (HAdd.hAdd (α := M) (β := M) (⁅⁅z, x⁆, (a : (a : L) → M) y⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M) -
                HAdd.hAdd (α := M) (β := M) (⁅⁅z, y⁆, (a : (a : L) → M) x⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
              (⁅z, (a : (a : L) → M) ⁅x, y⁆⁆ : M) -
          HSub.hSub (β := M)
            (HSub.hSub (β := M)
              (HSub.hSub (α := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M)
                (HAdd.hAdd (α := M) (β := M) (⁅⁅y, x⁆, (a : (a : L) → M) z⁆ : M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M)))
              (⁅z, (a : (a : L) → M) ⁅x, y⁆⁆ : M))
            ((a : (a : L) → M) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : M) +
        HSub.hSub (β := M)
          (HSub.hSub (β := M)
            (HSub.hSub (α := M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M)
              (HAdd.hAdd (α := M) (β := M) (⁅⁅z, x⁆, (a : (a : L) → M) y⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M)))
            (⁅y, (a : (a : L) → M) ⁅x, z⁆⁆ : M))
          ((a : (a : L) → M) (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆) : M) -
      HSub.hSub (β := M)
        (HSub.hSub (β := M)
          (HSub.hSub (α := M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M)
            (HAdd.hAdd (α := M) (β := M) (⁅⁅z, y⁆, (a : (a : L) → M) x⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M)))
          (⁅x, (a : (a : L) → M) ⁅y, z⁆⁆ : M))
        ((a : (a : L) → M) (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) : M) =
    0
have h : HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M))
              (-⁅x, (a : (a : L) → M) ⁅z, y⁆⁆ : M) -
            HSub.hSub (β := M)
              (HSub.hSub (α := M) (β := M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
              (-⁅y, (a : (a : L) → M) ⁅z, x⁆⁆ : M) +
          HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
            (-⁅z, (a : (a : L) → M) ⁅y, x⁆⁆ : M) -
        (HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M))
            (-⁅z, (a : (a : L) → M) ⁅y, x⁆⁆ : M) -
          HSub.hSub (α := M) (-(a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M)
            (-HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M))) +
      (HSub.hSub (β := M)
          (HSub.hSub (α := M) (β := M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M))
          (-⁅y, (a : (a : L) → M) ⁅z, x⁆⁆ : M) -
        HSub.hSub (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) (-(a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)) -
    (HSub.hSub (β := M)
        (HSub.hSub (α := M) (β := M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
        (-⁅x, (a : (a : L) → M) ⁅z, y⁆⁆ : M) -
      HSub.hSub (β := M)
        (HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M))
        ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)) =
  0
Tactic: simp only [lie_lie, sub_add_cancel, map_sub, ← lie_skew x y, ← lie_skew x z, ← lie_skew y z,
    lie_neg, map_neg, this]