refactor(Algebra/Polynomial/Splits): begin deprecation (#32040)

This PR begins the deprecation in `Splits.lean` as we move over to the new API in `Factors.lean`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Algebra/Polynomial/Splits.lean

@@ -41,29 +41,30 @@ section CommRing
 variable [CommRing K] [Field L] [Field F]
 variable (i : K →+* L)
 
-theorem splits_zero : Splits (0 : K[X]) := by
-  simp
+@[deprecated (since := "2025-11-24")]
+alias splits_zero := Splits.zero
 
-theorem splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : Splits (f.map i) := by
-  simp [h]
+@[deprecated "Use `Splits.C` instead." (since := "2025-11-24")]
+theorem splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : Splits (f.map i) :=
+  h ▸ Splits.C a
 
-theorem splits_C (a : K) : Splits (C a) := by
-  simp
+@[deprecated (since := "2025-11-24")]
+alias splits_C := Splits.C
 
-theorem splits_of_map_degree_eq_one {f : K[X]} (hf : degree (f.map i) = 1) : Splits (f.map i) :=
-  Splits.of_degree_eq_one hf
+@[deprecated (since := "2025-11-24")]
+alias splits_of_map_degree_eq_one := Splits.of_degree_eq_one
 
-theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits (f.map i) :=
-  Splits.of_degree_le_one (degree_map_le.trans hf)
+@[deprecated (since := "2025-11-24")]
+alias splits_of_degree_le_one := Splits.of_degree_le_one
 
-theorem splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : Splits (f.map i) :=
-  splits_of_degree_le_one i hf.le
+@[deprecated (since := "2025-11-24")]
+alias splits_of_degree_eq_one := Splits.of_degree_eq_one
 
-theorem splits_of_natDegree_le_one {f : K[X]} (hf : natDegree f ≤ 1) : Splits (f.map i) :=
-  splits_of_degree_le_one i (degree_le_of_natDegree_le hf)
+@[deprecated (since := "2025-11-24")]
+alias splits_of_natDegree_le_one := Splits.of_natDegree_le_one
 
-theorem splits_of_natDegree_eq_one {f : K[X]} (hf : natDegree f = 1) : Splits (f.map i) :=
-  splits_of_natDegree_le_one i (le_of_eq hf)
+@[deprecated (since := "2025-11-24")]
+alias splits_of_natDegree_eq_one := Splits.of_natDegree_eq_one
 
 theorem splits_mul {f g : K[X]} (hf : Splits (f.map i)) (hg : Splits (g.map i)) :
     Splits ((f * g).map i) := by
@@ -74,106 +75,78 @@ theorem splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Spli
   simp only [Splits, Polynomial.map_mul, mul_ne_zero_iff] at hfg h
   exact (splits_mul_iff hfg.1 hfg.2).mp h
 
+@[deprecated "Use `Polynomial.map_map` instead." (since := "2025-11-24")]
 theorem splits_map_iff {L : Type*} [CommRing L] (i : K →+* L) (j : L →+* F) {f : K[X]} :
     Splits ((f.map i).map j) ↔ Splits (f.map (j.comp i)) := by
-  simp [Splits, Polynomial.map_map]
+  rw [Polynomial.map_map]
 
-theorem splits_one : Splits (map i 1) :=
-  map_C i ▸ splits_C _
+@[deprecated (since := "2025-11-24")]
+alias splits_one := Splits.one
 
 theorem splits_of_isUnit [IsDomain K] {u : K[X]} (hu : IsUnit u) : (u.map i).Splits :=
-  (isUnit_iff.mp hu).choose_spec.2 ▸ map_C i ▸ splits_C _
+  (isUnit_iff.mp hu).choose_spec.2 ▸ map_C i ▸ Splits.C _
 
-theorem splits_X_sub_C {x : K} : ((X - C x).map i).Splits :=
-  splits_of_degree_le_one _ <| degree_X_sub_C_le _
+@[deprecated (since := "2025-11-24")]
+alias splits_X_sub_C := Splits.X_sub_C
 
-theorem splits_X : (X.map i).Splits :=
-  splits_of_degree_le_one _ degree_X_le
+@[deprecated (since := "2025-11-24")]
+alias splits_X := Splits.X
 
-theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
-    (∀ j ∈ t, ((s j).map i).Splits) → ((∏ x ∈ t, s x).map i).Splits := by
-  classical
-  refine Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => ?_
-  rw [Finset.forall_mem_insert] at ht; rw [Finset.prod_insert hat]
-  exact splits_mul i ht.1 (ih ht.2)
+@[deprecated (since := "2025-11-24")]
+alias splits_prod := Splits.prod
 
-theorem splits_pow {f : K[X]} (hf : (f.map i).Splits) (n : ℕ) : ((f ^ n).map i).Splits := by
-  rw [← Finset.card_range n, ← Finset.prod_const]
-  exact splits_prod i fun j _ => hf
+@[deprecated (since := "2025-11-24")]
+alias splits_pow := Splits.pow
 
-theorem splits_X_pow (n : ℕ) : ((X ^ n).map i).Splits :=
-  splits_pow i (splits_X i) n
+@[deprecated (since := "2025-11-24")]
+alias splits_X_pow := Splits.X_pow
 
+@[deprecated "Use `Polynomial.map_id` instead." (since := "2025-11-24")]
 theorem splits_id_iff_splits {f : K[X]} :
     ((f.map i).map (RingHom.id L)).Splits ↔ (f.map i).Splits := by
-  rw [splits_map_iff, RingHom.id_comp]
+  rw [map_id]
 
 variable {i}
 
--- TODO: Prove the analogous composition theorems for `Factors`
-theorem Splits.comp_of_map_degree_le_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1)
-    (h : (f.map i).Splits) : ((f.comp p).map i).Splits := by
-  rw [splits_iff_splits] at h ⊢
-  by_cases hzero : map i (f.comp p) = 0
-  · exact Or.inl hzero
-  cases h with
-  | inl h0 =>
-    exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp
-  | inr h =>
-    right
-    intro g irr dvd
-    rw [map_comp] at dvd hzero
-    cases lt_or_eq_of_le hd with
-    | inl hd =>
-      rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
-      refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
-      simpa using hzero
-    | inr hd =>
-      let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
-          (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
-      rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
-      have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
-      rw [degree_eq_natDegree irr.ne_zero]
-      rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval,
-        degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
-        natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero),
-        natDegree_X_sub_C, mul_one] at this
-
-theorem splits_iff_comp_splits_of_degree_eq_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree = 1) :
-    (f.map i).Splits ↔ ((f.comp p).map i).Splits := by
-  rw [← splits_id_iff_splits, ← splits_id_iff_splits (f := f.comp p), map_comp]
-  refine ⟨fun h => Splits.comp_of_map_degree_le_one
-    (le_of_eq (map_id (R := L) ▸ hd)) h, fun h => ?_⟩
+theorem Splits.comp_of_degree_le_one {f : L[X]} {p : L[X]} (hd : p.degree ≤ 1)
+    (h : f.Splits) : (f.comp p).Splits := by
+  obtain ⟨m, hm⟩ := splits_iff_exists_multiset.mp h
+  rw [hm, mul_comp, C_comp, multiset_prod_comp]
+  refine (Splits.C _).mul (Splits.multisetProd ?_)
+  simp only [Multiset.mem_map]
+  rintro - ⟨-, ⟨a, -, rfl⟩, rfl⟩
+  apply Splits.of_degree_le_one
+  grw [sub_comp, X_comp, C_comp, degree_sub_le, hd, degree_C_le, max_eq_left zero_le_one]
+
+@[deprecated (since := "2025-11-24")]
+alias Splits.comp_of_map_degree_le_one := Splits.comp_of_degree_le_one
+
+theorem splits_iff_comp_splits_of_degree_eq_one {f : L[X]} {p : L[X]} (hd : p.degree = 1) :
+    f.Splits ↔ (f.comp p).Splits := by
+  refine ⟨Splits.comp_of_degree_le_one hd.le, fun h ↦ ?_⟩
   let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
       (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
-  have : (map i f) = ((map i f).comp (map i p)).comp ((C ⅟(map i p).leadingCoeff *
-      (X - C ((map i p).coeff 0)))) := by
+  have : f = (f.comp p).comp ((C ⅟p.leadingCoeff *
+      (X - C (p.coeff 0)))) := by
     rw [comp_assoc]
     nth_rw 1 [eq_X_add_C_of_degree_eq_one hd]
-    simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
+    simp only [invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
       ← mul_assoc]
     simp
-  refine this ▸ Splits.comp_of_map_degree_le_one ?_ h
-  simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := (map i p).leadingCoeff)))]
-
-/--
-This is a weaker variant of `Splits.comp_of_map_degree_le_one`,
-but its conditions are easier to check.
--/
-theorem Splits.comp_of_degree_le_one {f : K[X]} {p : K[X]} (hd : p.degree ≤ 1)
-    (h : (f.map i).Splits) : ((f.comp p).map i).Splits :=
-  Splits.comp_of_map_degree_le_one (degree_map_le.trans hd) h
+  rw [this]
+  refine Splits.comp_of_degree_le_one ?_ h
+  simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := p.leadingCoeff)))]
 
-theorem Splits.comp_X_sub_C (a : K) {f : K[X]}
-    (h : (f.map i).Splits) : ((f.comp (X - C a)).map i).Splits :=
+theorem Splits.comp_X_sub_C (a : L) {f : L[X]}
+    (h : f.Splits) : (f.comp (X - C a)).Splits :=
   Splits.comp_of_degree_le_one (degree_X_sub_C_le _) h
 
-theorem Splits.comp_X_add_C (a : K) {f : K[X]}
-    (h : (f.map i).Splits) : ((f.comp (X + C a)).map i).Splits :=
-  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (-a)) h
+theorem Splits.comp_X_add_C (a : L) {f : L[X]}
+    (h : f.Splits) : (f.comp (X + C a)).Splits :=
+  Splits.comp_of_degree_le_one (degree_X_add_C a).le h
 
-theorem Splits.comp_neg_X {f : K[X]} (h : (f.map i).Splits) : ((f.comp (-X)).map i).Splits :=
-  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (0 : K)) h
+theorem Splits.comp_neg_X {f : L[X]} (h : f.Splits) : (f.comp (-X)).Splits :=
+  Splits.comp_of_degree_le_one (by rw [degree_neg, degree_X]) h
 
 variable (i)
 
@@ -246,7 +219,7 @@ theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
   classical
   refine
     Finset.induction_on t (fun _ =>
-        ⟨fun _ _ h => by simp only [Finset.notMem_empty] at h, fun _ => splits_one i⟩)
+        ⟨fun _ _ h => by simp only [Finset.notMem_empty] at h, by simp⟩)
       fun a t hat ih ht => ?_
   rw [Finset.forall_mem_insert] at ht ⊢
   rw [Finset.prod_insert hat, Polynomial.map_mul, splits_mul_iff (map_ne_zero ht.1)
@@ -430,7 +403,7 @@ theorem splits_id_of_splits {f : K[X]} (h : Splits (f.map i))
 
 theorem splits_comp_of_splits (i : R →+* K) (j : K →+* L) {f : R[X]} (h : Splits (f.map i)) :
     Splits (f.map (j.comp i)) :=
-  (splits_map_iff i j).mp (splits_of_splits_id _ <| (splits_map_iff i <| .id K).mpr h)
+  f.map_map i j ▸ h.map j
 
 variable [Algebra R K] [Algebra R L]
 

Mathlib/FieldTheory/AbelRuffini.lean

@@ -181,8 +181,9 @@ theorem gal_X_pow_sub_C_isSolvable (n : ℕ) (x : F) : IsSolvable (X ^ n - C x).
   · exact gal_X_pow_sub_one_isSolvable n
   · rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]
     apply gal_X_pow_sub_C_isSolvable_aux
+    rw [map_id]
     have key := SplittingField.splits (X ^ n - 1 : F[X])
-    rwa [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, map_X,
+    rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
       Polynomial.map_one] at key
 
 end GalXPowSubC

Mathlib/FieldTheory/Fixed.lean

@@ -259,11 +259,11 @@ variable [Finite G]
 instance normal : Normal (FixedPoints.subfield G F) F where
   isAlgebraic x := (isIntegral G F x).isAlgebraic
   splits' x :=
-    (Polynomial.splits_id_iff_splits _).1 <| by
+    by
       cases nonempty_fintype G
       rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
         Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]
-      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _
+      exact Polynomial.Splits.prod fun _ _ => Polynomial.Splits.X_sub_C _
 
 instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := by
   classical

Mathlib/FieldTheory/Galois/Basic.lean

@@ -524,7 +524,7 @@ theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.I
   rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]
   · exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2
   · refine Polynomial.splits_of_splits_of_dvd _ (Polynomial.map_ne_zero h1) ?_ h2
-    rw [Polynomial.splits_map_iff, ← IsScalarTower.algebraMap_eq]
+    rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
     exact sp.splits
 
 theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :
@@ -547,7 +547,7 @@ theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separ
   · have key := IntermediateField.card_algHom_adjoin_integral F (K := E)
       (show IsIntegral F (0 : E) from isIntegral_zero)
     rw [IsSeparable, minpoly.zero, Polynomial.natDegree_X] at key
-    specialize key Polynomial.separable_X (Polynomial.splits_X (algebraMap F E))
+    specialize key Polynomial.separable_X (Polynomial.Splits.X.map (algebraMap F E))
     rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
     refine Eq.trans ?_ key
     apply Nat.card_congr
@@ -584,7 +584,7 @@ theorem sup_right (K L : IntermediateField F E) [IsGalois F K] [FiniteDimensiona
   suffices T'.IsSplittingField L E from IsGalois.of_separable_splitting_field (p := T') hT₁.map
   rw [isSplittingField_iff_intermediateField] at hT₂ ⊢
   constructor
-  · rw [Polynomial.splits_map_iff, ← IsScalarTower.algebraMap_eq]
+  · rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
     exact Polynomial.splits_of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)
   · have h' : T'.rootSet E = T.rootSet E := by simp [Set.ext_iff, Polynomial.mem_rootSet', T']
     rw [← lift_inj, lift_adjoin, ← coe_val, T.image_rootSet hT₂.1] at hT₂

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

@@ -151,9 +151,9 @@ theorem isSplittingField_iSup {p : ι → K[X]}
     (∏ i ∈ s, p i).IsSplittingField K (⨆ i ∈ s, t i : IntermediateField K L) := by
   let F : IntermediateField K L := ⨆ i ∈ s, t i
   have hF : ∀ i ∈ s, t i ≤ F := fun i hi ↦ le_iSup_of_le i (le_iSup (fun _ ↦ t i) hi)
-  simp only [isSplittingField_iff] at h ⊢
+  simp only [isSplittingField_iff, Polynomial.map_prod] at h ⊢
   refine
-    ⟨splits_prod (algebraMap K F) fun i hi ↦
+    ⟨Splits.prod fun i hi ↦
         splits_comp_of_splits (algebraMap K (t i)) (inclusion (hF i hi)).toRingHom
           (h i hi).1,
       ?_⟩

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -188,8 +188,8 @@ instance isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) :=
           simp⟩
 
 instance : IsAlgClosure k (AlgebraicClosure k) := .of_splits fun f hf _ ↦ by
-  rw [show f = (⟨f, hf⟩ : Monics k) from rfl, ← splits_id_iff_splits, Monics.map_eq_prod]
-  exact splits_prod _ fun _ _ ↦ (splits_id_iff_splits _).mpr (splits_X_sub_C _)
+  rw [show f = (⟨f, hf⟩ : Monics k) from rfl, Monics.map_eq_prod]
+  exact Splits.prod fun _ _ ↦ (Splits.X_sub_C _).map _
 
 instance isAlgClosed : IsAlgClosed (AlgebraicClosure k) := IsAlgClosure.isAlgClosed k
 

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -304,8 +304,7 @@ theorem IsAlgClosure.of_splits {R K} [CommRing R] [IsDomain R] [Field K] [Algebr
   isAlgebraic := inferInstance
   isAlgClosed := .of_exists_root _ fun _p _ p_irred ↦
     have ⟨g, monic, irred, dvd⟩ := p_irred.exists_dvd_monic_irreducible_of_isIntegral (K := R)
-    exists_root_of_splits _ (splits_of_splits_of_dvd _ (map_monic_ne_zero monic)
-      ((splits_id_iff_splits _).mpr <| h g monic irred) dvd) <|
+    Splits.exists_eval_eq_zero (Splits.of_dvd (h g monic irred) (map_monic_ne_zero monic) dvd) <|
         degree_ne_of_natDegree_ne p_irred.natDegree_pos.ne'
 
 namespace IsAlgClosed

Mathlib/FieldTheory/Isaacs.lean

@@ -46,7 +46,8 @@ theorem nonempty_algHom_of_exist_roots (h : ∀ x : E, ∃ y : K, aeval y (minpo
   have splits s (hs : s ∈ S) : ((minpoly F s).map (algebraMap F K')).Splits := by
     apply splits_of_splits_of_dvd _
       (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ minpoly.ne_zero <| (alg.isIntegral).1 _)
-      ((splits_map_iff _ _).mp <| SplittingField.splits p) (Finset.dvd_prod_of_mem _ hs)
+      (map_map (algebraMap F K) (algebraMap K p.SplittingField) _ ▸ SplittingField.splits p)
+      (Finset.dvd_prod_of_mem _ hs)
   let K₀ := (⊥ : IntermediateField K K').restrictScalars F
   let FS := adjoin F (S : Set E)
   let Ω := FS →ₐ[F] K'

Mathlib/FieldTheory/KummerExtension.lean

@@ -60,7 +60,7 @@ theorem X_pow_sub_C_splits_of_isPrimitiveRoot
     (X ^ n - C a).Splits := by
   cases n.eq_zero_or_pos with
   | inl hn =>
-    simp only [hn, pow_zero, ← C.map_one, ← map_sub, splits_C]
+    simp only [hn, pow_zero, ← C.map_one, ← map_sub, Splits.C]
   | inr hn =>
     rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
 

Mathlib/FieldTheory/Normal/Basic.lean

@@ -38,8 +38,8 @@ theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K]
   classical
   let s := Module.Basis.ofVectorSpace F K
   refine
-    ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x),
-      Subalgebra.toSubmodule.injective ?_⟩
+    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
+      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
   rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
   refine fun x =>
     Algebra.subset_adjoin
@@ -80,7 +80,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] :
       rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
             IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
       exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
-    · rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]; exact hL.1
+    · rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]; exact hL.1
   · rw [Polynomial.map_ne_zero_iff (algebraMap F L).injective, mul_ne_zero_iff]
     exact ⟨hp, minpoly.ne_zero hx⟩
 
@@ -191,7 +191,7 @@ noncomputable def AlgHom.liftNormal [h : Normal F E] : E →ₐ[F] E :=
         ((IsScalarTower.toAlgHom F K₂ E).comp ϕ).toRingHom.toAlgebra _
         (fun x _ ↦ ⟨(h.out x).1.tower_top,
           splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
-            (by rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]
+            (by rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
                 exact (h.out x).2)
             (minpoly.dvd_map_of_isScalarTower F K₁ x)⟩)
         (IntermediateField.adjoin_univ _ _)
@@ -291,5 +291,5 @@ instance Algebra.IsQuadraticExtension.normal (F K : Type*) [Field F] [Field K] [
   splits' := by
     intro x
     obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
-    · exact splits_of_natDegree_le_one _ (by rwa [Nat.le_iff_lt_add_one])
+    · exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (by rwa [Nat.le_iff_lt_add_one])
     · exact splits_of_natDegree_eq_two _ h (minpoly.aeval F x)