Commit 2023-11-10 20:41 9cc270f8

refactor: golf IntermediateField.Lifts (#8221) Inspired by the IsAlgClosed.lift.SubfieldWithHom counterpart:

• Change Lifts from a Sigma type to a structure with fields carrier and emb.
• Change the definition of the partial order on Lifts to use IntermediateField.inclusion.
• Use Subalgebra.iSupLift in the proof of Lifts.exists_upper_bound. Also:
• Inline multiple auxiliary definitions for Lifts.exists_upper_bound and Lifts.exists_lift_of_splits into the proofs proper.
• Move the Supremum section much further up, in order to use the new lemma toSubalgebra_iSup_of_directed to prove stuff about Lifts (and golf a proof about CompactElement). isAlgebraic_iSup however can't be moved up, so I put it near adjoin.finiteDimensional, the last lemma it depends on.