-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma isNilpotent_toEnd_sub_algebraMap [IsNoetherian R M] (χ : L → R) (x : L) :
    _root_.IsNilpotent <| toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Tactic:
have : toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) =
    (toEnd R L M x - algebraMap R _ (χ x)).restrict
      (fun m hm ↦ sub_mem (LieSubmodule.lie_mem _ hm) (Submodule.smul_mem _ _ hm)) := by
  rfl

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Tactic:
use k

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
⊢ ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x)) ^ k = 0

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Tactic:
obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Proof state:
case h.h.mk.a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
m : M
hm : m ∈ genWeightSpace M χ
⊢ ↑((((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x)) ^ k) ⟨m, hm⟩) =
    ↑(0 ⟨m, hm⟩)

Tactic:
simp only [this, LinearMap.pow_restrict _, LinearMap.zero_apply, ZeroMemClass.coe_zero,
  ZeroMemClass.coe_eq_zero]

Result:
case h.h.mk.a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
m : M
hm : m ∈ genWeightSpace M χ
⊢ ((((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k).restrict ⋯) ⟨m, hm⟩ = 0

Proof state:
case h.h.mk.a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
m : M
hm : m ∈ genWeightSpace M χ
⊢ ((((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k).restrict ⋯) ⟨m, hm⟩ = 0

Tactic:
exact ZeroMemClass.coe_eq_zero.mp (hk hm)

Result:
no goals