no goals
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
⊢ IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M ↔ IsNilpotent R L M
constructor <;> rintro ⟨k, hk⟩ <;> use k <;>
    rw [← LieSubmodule.coe_toSubmodule_eq_iff] at hk ⊢ <;>
  simpa using hk