-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
calc_1 :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (β := End R M)
          (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
            HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) :
      R)
calc_2 :
  (trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (β := End R M)
        (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
          HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
calc_3 :
  HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
        R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆ : R)
have calc_4 : HSub.hSub (α := R) (β := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
          (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
          (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
      R) =
  (((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆
Tactic: calc traceForm R L M ⁅x, y⁆ z
      = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
    _ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
    _ = traceForm R L M x ⁅y, z⁆ := ?_