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
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑N
⊢ ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N
simpa using N.lie_mem hm