-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) ⁅x, y⁆ = 0
rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        ⁅x, y⁆ :
      R)
    (0 : R)
rw₄ :
  Eq.{u_2 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        ((((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              (a : L) → ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ))
            ⁅x, y⁆ :
          ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) :
      R)
    (0 : R)
rw₅ :
  Eq.{u_2 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
              (a : L) → End R ↥(genWeightSpace M χ))
            ⁅x, y⁆ :
          End R ↥(genWeightSpace M χ)) :
      R)
    (0 : R)
rw₆ :
  Eq.{u_2 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (Bracket.bracket (L := End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                x :
              End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              y) :
          End R ↥(genWeightSpace M χ)) :
      R)
    (0 : R)
rw₇ :
  Eq.{u_2 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HMul.hMul (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                x :
              End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                y :
              End R ↥(genWeightSpace M χ)) -
          HMul.hMul (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                y :
              End R ↥(genWeightSpace M χ))
            (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                    LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                  (a : L) → End R ↥(genWeightSpace M χ))
                x :
              End R ↥(genWeightSpace M χ))) :
      R)
    (0 : R)
⊢ χ ⁅x, y⁆ = 0
have rw₈ : HSub.hSub (α := R) (β := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HMul.hMul (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              x :
            End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              y :
            End R ↥(genWeightSpace M χ))) :
      R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HMul.hMul (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              y :
            End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              x :
            End R ↥(genWeightSpace M χ))) :
      R) =
  0
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]