∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] (U : LieSubalgebra K L)
  (x : L) (hxU : x ∈ U) (hUle : U ≤ ↑⟨LieSubalgebra.engel K x, ⋯⟩),
  IsScalarTower K K (L ⧸ { toSubmodule := (LieSubalgebra.engel K x).toSubmodule, lie_mem := ⋯ })