-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
h :
  ∀ (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)
⊢ 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 =
    0

Tactic:
ext ⟨m, hm⟩