-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
mem :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M)
          (Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b) :
            End R M)
          y) :
      R)
    (0 : R)
mem₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (Bracket.bracket (L := M →ₗ[R] M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y)) :
      R)
    (0 : R)
mem₂ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y -
            HMul.hMul (β := M →ₗ[R] M) y
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M))) :
      R)
    (0 : R)
mem₃ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (Bracket.bracket (L := M →ₗ[R] M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y)) :
      R)
    (0 : R)
mem₄ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (Bracket.bracket (L := M →ₗ[R] M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y)) :
      R)
    (0 : R)
mem₅ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (-((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := 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) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have mem₆ : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (-HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)) :
    R)
  (0 : R)
Tactic: rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]