∀ (K : Type u_7) {L : Type u_8} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : Module.Finite K L] (x : L), LieAlgebra.rank K L ≤ Module.finrank K ↥(LieSubalgebra.engel K x)