engel_isBot_of_isMin

Stream: mathlib4

[Kim Morrison]

Would anyone be interested in refactoring engel_isBot_of_isMin in Mathlib/Algebra/Lie/CartanExists.lean into smaller pieces? I'm encountering errors on nightly-testing, and the proof is unmanageably long. (> 200 lines)

[Johan Commelin]

I guess that is my duty. Will look into it asap.

[Kim Morrison]

Oh -- I fixed the problem on nightly-testing, so it is much less urgent now. :-)

[Johan Commelin]

Aah, ok. Was it a nasty fix that needs backporting? Or can this just be part of the final bump?

[Kim Morrison]

I backported it already as part of #13551. It just needed an argument filled in, because something weird has changed with E vs engel ....