∀ {F : Type u_1} {K : Type u_3} (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F]
  [inst_3 : Algebra K L] [inst_4 : Algebra K F] (f : Polynomial K),
  (Polynomial.map (algebraMap K F) f).Splits → ¬f = 0 → Nonempty (↥(Algebra.adjoin K ↑(f.aroots L).toFinset) →ₐ[K] F)