refactor: golf IntermediateField.Lifts (#8221)

Inspired by the [IsAlgClosed.lift.SubfieldWithHom](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/Basic.html#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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Algebra/Subalgebra/Basic.html#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.



Co-authored-by: acmepjz <acme_pjz@hotmail.com>

Mathlib/FieldTheory/AbelRuffini.lean

@@ -341,13 +341,14 @@ theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (
   have hpq := Polynomial.splits_of_splits_mul _
     (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
     (SplittingField.splits (p * q))
-  let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice <| algHom_mk_adjoin_splits (by
-    intro x hx
-    cases' hx with hx hx
-    rw [hx]
-    exact ⟨isIntegral α, hpq.1⟩
-    cases hx
-    exact ⟨isIntegral β, hpq.2⟩)
+  let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField :=
+    Classical.choice <| nonempty_algHom_adjoin_of_splits <| by
+      intro x hx
+      cases' hx with hx hx
+      rw [hx]
+      exact ⟨isIntegral α, hpq.1⟩
+      cases hx
+      exact ⟨isIntegral β, hpq.2⟩
   have key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩) := by
     refine' minpoly.eq_of_irreducible_of_monic
       (minpoly.irreducible (isIntegral γ)) _ (minpoly.monic (isIntegral γ))