-- 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 : IsNoetherian R M
χ : L → R
x : L
this :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯
k : ℕ
hk :
  (↑(genWeightSpace M χ) : Submodule R M) ≤
    LinearMap.ker
      (HSub.hSub (α := Module.End R M) (β := Module.End R M)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
          ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
        k)
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
⊢ Eq.{u_4 + 1} (α := M)
    (↑((HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
                (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                        LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
                      (a : L) → Module.End R ↥(genWeightSpace M χ))
                    x :
                  Module.End R ↥(genWeightSpace M χ))
                ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ))
                    (χ x) :
                  Module.End R ↥(genWeightSpace M χ)) ^
              k :
            (a : ↥(genWeightSpace M χ)) → ↥(genWeightSpace M χ))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) x) m hm)) :
      M)
    (↑((0 : (a : ↥(genWeightSpace M χ)) → ↥(genWeightSpace M χ))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) x) m hm)) :
      M)
have h : Eq (α := ↥(genWeightSpace M χ))
  (((HSub.hSub (α := Module.End R M) (β := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
              k).restrict
          sorry :
        (a : ↥(genWeightSpace M χ)) → ↥(genWeightSpace M χ))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) x) m hm) :
    ↥(genWeightSpace M χ))
  (0 : ↥(genWeightSpace M χ))
Tactic: simp only [this, Module.End.pow_restrict _, LinearMap.zero_apply, ZeroMemClass.coe_zero,
    ZeroMemClass.coe_eq_zero]