chore(algebra/lie/engel): speed up proof of Engel's theorem slightly (#…

…12205)

Local measurements using `set_option profiler true` are noisy but indicate
that this speeds up elaboration of `lie_algebra.is_engelian_of_is_noetherian`
by about 20% from about 10s to about 8s.

src/algebra/lie/engel.lean

@@ -254,7 +254,8 @@ begin
       exact submodule.quotient.nontrivial_of_lt_top _ hK₂.lt_top, },
     haveI : lie_module.is_nilpotent R K (L' ⧸ K.to_lie_submodule),
     { refine hK₁ _ (λ x, _),
-      exact module.End.is_nilpotent.mapq _ (lie_algebra.is_nilpotent_ad_of_is_nilpotent (h x)), },
+      have hx := lie_algebra.is_nilpotent_ad_of_is_nilpotent (h x),
+      exact module.End.is_nilpotent.mapq _ hx, },
     exact nontrivial_max_triv_of_is_nilpotent R K (L' ⧸ K.to_lie_submodule), },
   haveI _i5 : is_noetherian R L' :=
     is_noetherian_of_surjective L _ (linear_map.range_range_restrict (to_endomorphism R L M)),