-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
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 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
this :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HSub.hSub (α := 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 χ))
          (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id)) :
      R)
    (0 : R)
rwa :
  ∀
    (this :
      HSub.hSub (α := R) (β := R)
          ((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 :
                End R ↥(genWeightSpace M χ)) :
            R)
          ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
              (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id) :
            R) =
        0),
    (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 :
          End R ↥(genWeightSpace M χ)) =
      finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
⊢ (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 :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
have rwa₁ : ∀
  (this :
    HSub.hSub (α := R)
        ((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 :
              End R ↥(genWeightSpace M χ)) :
          R)
        (HSMul.hSMul (β := R) (χ x)
          ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R) LinearMap.id :
            R)) =
      0),
  (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 :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
Tactic: rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
      ← nsmul_eq_mul] at this
Cleared hypotheses: this