Core: consolidate onto Mathlib's Splits API and general interlacing lemmas

PROOF_STATUS.md

@@ -30,7 +30,7 @@ None.
 | Liu theorem with common roots | `compatible_iff_rootCountBranchesWithCommon` |
 | Garloff--Wagner PF closure | `garloffWagnerHadamardPFInterl_of_nonnegStrictInterl` |
 | Bounded-degree polar-theta interlacing preservation | `polarThetaPreservesInterlStatement`, witnessed by `polarTheta_preserves_interl` |
-| Theta interlacing preservation on the PF cone | `thetaPreservesInterlStatement`, witnessed by `thetaPreservesInterl` |
+| Theta interlacing preservation | `thetaPreservesInterlStatement`, witnessed by `Interl.theta` |
 | Derivative preservation of weak interlacing | `derivativePreservesInterl` |
 | Nonnegative interlacing pair gives a Hurwitz-stable odd/even polynomial | `isHurwitzStable_oddEvenPolynomial_of_strictInterl` |
 | Hurwitz-stable odd/even polynomial gives an interlacing pair (issue #1112) | `strictInterl_of_isHurwitzStable_oddEvenPolynomial`, `isHurwitzStable_oddEvenPolynomial_iff` |

RealRooted/AffineDerivative.lean

@@ -682,7 +682,7 @@ lemma roots_card_of_sub_pred {p : ℝ[X]} (hp : p ≠ 0)
   have h1 : p.roots.card ≤ p.natDegree := card_roots' p
   have h2 : S.card ≤ p.roots.card := Multiset.card_le_card hle
   have hne_card : p.roots.card ≠ p.natDegree :=
-    fun h => hne (splits_of_card_roots h)
+    fun h => hne (Polynomial.splits_iff_card_roots.mpr h)
   -- p.roots.card = natDegree - 1
   have hrc : p.roots.card = p.natDegree - 1 := by lia
   -- Factor p = rprod * q where rprod = ∏(X - C r) for r ∈ p.roots
@@ -708,7 +708,7 @@ lemma roots_card_of_sub_pred {p : ℝ[X]} (hp : p ≠ 0)
     rw [natDegree_multiset_prod_X_sub_C_eq_card, hrc, ← hpq] at h3
     lia
   have hq_split := (isRealRooted_of_degree_one hq_deg).2
-  have hq_card := card_roots_of_splits hq_split
+  have hq_card := Polynomial.splits_iff_card_roots.mp hq_split
   rw [hq_empty, Multiset.card_zero, hq_deg] at hq_card
   lia
 
@@ -754,7 +754,7 @@ private lemma strictInterl_of_extra_root_left {f g : ℝ[X]} (hf₀ : f ≠ 0) (
     (hu : u ≤ r₁) :
     StrictInterl g f := by
   have hss_sorted : ss.Pairwise (· ≤ ·) :=
-    sorted_of_listInterlaces ss (r₁ :: rest) hrs_sorted hint
+    pairwise_le_of_listInterlaces ss (r₁ :: rest) hint
   have hu_le_all : ∀ s ∈ ss, u ≤ s :=
     fun s hs => le_trans hu (listInterlaces_all_ge ss rest r₁ hint s hs)
   have hug_sorted : (u :: ss).Pairwise (· ≤ ·) := by simp_all
@@ -781,7 +781,8 @@ theorem strictInterl_affine_derivative {f : ℝ[X]} (hf : f.Splits)
   set rs := f.roots.sort (· ≤ ·) with hrs_def
   have hrs_sorted : rs.Pairwise (· ≤ ·) := Multiset.pairwise_sort ..
   have hrs_eq : (↑rs : Multiset ℝ) = f.roots := Multiset.sort_eq ..
-  have hrs_length : rs.length = d := by rw [hrs_def, Multiset.length_sort, card_roots_of_splits hf]
+  have hrs_length : rs.length = d := by
+    rw [hrs_def, Multiset.length_sort, Polynomial.splits_iff_card_roots.mp hf]
   have hrs_root : ∀ r ∈ rs, f.IsRoot r := by simp_all
   have hsub_rs : (↑rs : Multiset ℝ) ≤ f.roots := le_of_eq hrs_eq
   have hgap_rs : ConsecNoRoots f rs := consecNoRoots_of_sorted_eq hrs_eq hrs_sorted
@@ -812,7 +813,7 @@ theorem strictInterl_affine_derivative {f : ℝ[X]} (hf : f.Splits)
     roots_card_of_sub_pred hg₀.ne_zero hss_sub (by
       rw [Multiset.coe_card, hss_length, hg_deg]; lia)
   have hss_eq_card : (↑ss : Multiset ℝ).card + 1 = g.roots.card := by
-    rw [Multiset.coe_card, hss_length, card_roots_of_splits hg_rr, hg_deg]
+    rw [Multiset.coe_card, hss_length, Polynomial.splits_iff_card_roots.mp hg_rr, hg_deg]
     lia
   obtain ⟨r₁, rest, hrs_cons⟩ : ∃ r₁ rest, rs = r₁ :: rest := by
     cases h : rs with
@@ -937,7 +938,7 @@ theorem strictInterl_affine_derivative {f : ℝ[X]} (hf : f.Splits)
       calc
         m = f.roots.count r₁ := by lia
         _ ≤ f.roots.card := Multiset.count_le_card _ _
-        _ = d := by rw [card_roots_of_splits hf, hd_def]
+        _ = d := by rw [Polynomial.splits_iff_card_roots.mp hf, hd_def]
     have hq_deg : q.natDegree = d - m := by
       have hdegmul :=
           natDegree_mul (p := (X - C r₁) ^ m) (q := q)
@@ -953,11 +954,11 @@ theorem strictInterl_affine_derivative {f : ℝ[X]} (hf : f.Splits)
       lia
     have hcard_step : qg.roots.card = q.roots.card + 1 := by
       calc
-        qg.roots.card = qg.natDegree := card_roots_of_splits hqg_rr.2
+        qg.roots.card = qg.natDegree := Polynomial.splits_iff_card_roots.mp hqg_rr.2
         _ = d - (m - 1) := hqg_deg
         _ = d - m + 1 := by lia
         _ = q.natDegree + 1 := by lia
-        _ = q.roots.card + 1 := by rw [← card_roots_of_splits hq_rr.2]
+        _ = q.roots.card + 1 := by rw [← Polynomial.splits_iff_card_roots.mp hq_rr.2]
     have hPg_nonneg' : 0 ≤ -(((-1 : ℝ) ^ q.roots.card) * Pg) := by
       rw [hcard_step, pow_add, pow_one, mul_neg_one] at hPg_nonneg
       grind
@@ -970,8 +971,8 @@ theorem strictInterl_affine_derivative {f : ℝ[X]} (hf : f.Splits)
       have hmulp' : 0 ≤ -(Pg * Pq) := by nlinarith [hmulp, hsquare]
       linarith
     have hEval_nonpos : qg.eval r₁ * q.eval r₁ ≤ 0 := by
-      rw [eval_eq_leadingCoeff_mul_prod_sub hqg_rr.2 r₁,
-        eval_eq_leadingCoeff_mul_prod_sub hq_rr.2 r₁,
+      rw [Polynomial.Splits.eval_eq_prod_roots hqg_rr.2 r₁,
+        Polynomial.Splits.eval_eq_prod_roots hq_rr.2 r₁,
         show (q.roots.map (r₁ - ·)).prod = Pq by lia,
         show (qg.roots.map (r₁ - ·)).prod = Pg by lia]
       have hlc_pos : 0 < qg.leadingCoeff * q.leadingCoeff :=
@@ -1008,9 +1009,11 @@ theorem strictInterl_affine_derivative_deg_one {f : ℝ[X]} (hf : f.Splits)
     exact mul_pos (by simp_all) hf₀
   -- f and g each have exactly one root
   obtain ⟨r, hr_eq⟩ :=
-    Multiset.card_eq_one.mp (show f.roots.card = 1 by rw [card_roots_of_splits hf, hdeg])
+    Multiset.card_eq_one.mp (show f.roots.card = 1 by
+      rw [Polynomial.splits_iff_card_roots.mp hf, hdeg])
   obtain ⟨s, hs_eq⟩ :=
-    Multiset.card_eq_one.mp (show g.roots.card = 1 by rw [card_roots_of_splits hg_rr.2, hg_deg])
+    Multiset.card_eq_one.mp (show g.roots.card = 1 by
+      rw [Polynomial.splits_iff_card_roots.mp hg_rr.2, hg_deg])
   have hr_root : f.IsRoot r :=
     (mem_roots hf₀.ne_zero).mp (hr_eq ▸ Multiset.mem_singleton_self r)
   have hr_nonpos : r ≤ 0 := hroots_nonpos r (hr_eq ▸ Multiset.mem_singleton_self r)
@@ -1026,7 +1029,7 @@ theorem strictInterl_affine_derivative_deg_one {f : ℝ[X]} (hf : f.Splits)
     exact hf₀
   -- g(r) = lc(g) * (r - s)
   have hgr_eq : g.eval r = g.leadingCoeff * (r - s) := by
-    rw [eval_eq_leadingCoeff_mul_prod_sub hg_rr.2 r, hs_eq]; simp
+    rw [Polynomial.Splits.eval_eq_prod_roots hg_rr.2 r, hs_eq]; simp
   -- s ≤ r
   have hsr : s ≤ r := by
     have : 0 < r - s := by simp_all

RealRooted/AffineFamily.lean

@@ -111,8 +111,7 @@ private lemma natDegree_shifted_pair_eq_succ_of_affine_family
   rcases lt_or_eq_of_le hdeg_right with hlt | heq
   · have hg_lt : g.natDegree < (X * f).natDegree := by simp_all
     have hsum_deg : (g + X * f).natDegree = (X * f).natDegree :=
-      natDegree_add_eq_right_of_natDegree_lt_of_posLeadingCoeff
-        hg_lt hXf_pos
+      Polynomial.natDegree_add_eq_right_of_natDegree_lt hg_lt
     simp_all
   · have hg_eq : g.natDegree = (X * f).natDegree := by simp_all
     have hsum_deg : (g + X * f).natDegree = (X * f).natDegree :=
@@ -143,8 +142,7 @@ private lemma strictInterl_of_strictInterl_shifted_pair_sameDegree
       (hfnn.pos_leadingCoeff hf0).X_mul
     have hg_lt : g.natDegree < (X * f).natDegree := by lia
     have hsum_deg : (g + X * f).natDegree = (X * f).natDegree :=
-      natDegree_add_eq_right_of_natDegree_lt_of_posLeadingCoeff
-        hg_lt hXf_pos
+      Polynomial.natDegree_add_eq_right_of_natDegree_lt hg_lt
     lia
   let a : ℝ := f.leadingCoeff⁻¹
   have ha_ne : a ≠ 0 := inv_ne_zero (ne_of_gt hf_pos)
@@ -717,20 +715,22 @@ lemma isRealRooted_affine_factor {s t : ℝ} (hs : 0 < s) :
 
 lemma affine_family_of_zero_left {g : ℝ[X]} (hg_ne : g ≠ 0) (hg_splits : g.Splits) :
     ∀ {s t : ℝ}, 0 < s → 0 < t →
-      ((((C s * X + C t) * (0 : ℝ[X])) + g) ≠ 0 ∧ (((C s * X + C t) * (0 : ℝ[X])) + g).Splits) := by
+      ((((C s * X + C t) * (0 : ℝ[X])) + g) ≠ 0 ∧
+        (((C s * X + C t) * (0 : ℝ[X])) + g).Splits) := by
   simp [*]
 
 lemma affine_family_of_zero_right {f : ℝ[X]} (hf_ne : f ≠ 0) (hf_splits : f.Splits) :
     ∀ {s t : ℝ}, 0 < s → 0 < t →
-      ((((C s * X + C t) * f) + (0 : ℝ[X])) ≠ 0 ∧ (((C s * X + C t) * f) + (0 : ℝ[X])).Splits) := by
+      ((((C s * X + C t) * f) + (0 : ℝ[X])) ≠ 0 ∧
+        (((C s * X + C t) * f) + (0 : ℝ[X])).Splits) := by
   intro s t hs ht
   simpa using isRealRooted_mul (isRealRooted_affine_factor (t := t) hs).1
     (isRealRooted_affine_factor (t := t) hs).2 hf_ne hf_splits
 
 lemma hasNonnegCoeffs_affine_linear {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
     HasNonnegCoeffs (C a * X + C b) := by
   have hCb : HasNonnegCoeffs (C b) := by rintro (_ | n) <;> simp [hb]
-  exact (nonnegCoeffs_C_mul ha hasNonnegCoeffs_X).add hCb
+  exact (hasNonnegCoeffs_C_mul ha hasNonnegCoeffs_X).add hCb
 
 lemma interl_one_affine_linear {a b : ℝ} (ha : 0 < a) :
     Interl (1 : ℝ[X]) (C a * X + C b) := by

RealRooted/AffineFamily/Basic.lean

@@ -91,7 +91,7 @@ theorem isRealRooted_affine_combo_of_strictInterl_nonneg {f g : ℝ[X]}
     StrictInterl.add_of_right_of_posLeadingCoeff hg_Xf hsXf hg_pos hsXf_pos
   have hmid_nonneg : HasNonnegCoeffs (g + C s * (X * f)) := by
     refine hgnn.add ?_
-    exact (nonnegCoeffs_C_mul hs.le hfnn.X_mul)
+    exact (hasNonnegCoeffs_C_mul hs.le hfnn.X_mul)
   have hmid_pos : HasPosLeadingCoeff (g + C s * (X * f)) :=
     hmid_nonneg.pos_leadingCoeff hmid.1.1
   have hsum : StrictInterl (C t * f + (g + C s * (X * f))) (X * f) :=

RealRooted/AffineFamily/Boundary.lean

@@ -42,7 +42,7 @@ private lemma affine_family_pair_data {f g : ℝ[X]}
     X * f ≠ 0 ∧
     HasPosLeadingCoeff (C t * f + g) ∧
     HasPosLeadingCoeff (X * f) := by
-  have hCt_nonneg : HasNonnegCoeffs (C t * f) := nonnegCoeffs_C_mul ht.le hfnn
+  have hCt_nonneg : HasNonnegCoeffs (C t * f) := hasNonnegCoeffs_C_mul ht.le hfnn
   have hsum_nonneg : HasNonnegCoeffs (C t * f + g) := hCt_nonneg.add hgnn
   have hXf_nonneg : HasNonnegCoeffs (X * f) := hfnn.X_mul
   have hsum_ne : C t * f + g ≠ 0 :=
@@ -106,8 +106,8 @@ protected theorem AffineFamily.isRealRooted_of_add_C_mul_right_family_of_natDegr
     simpa [δ, one_div] using tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)
   let p : ℕ → ℝ[X] := fun M => g₀ + C (δ M) * f₀
   have hp_deg (M : ℕ) : (p M).natDegree = g₀.natDegree :=
-    natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff
-      (by simpa [p, natDegree_C_mul (hδ_pos M).ne'] using hdeg₀) hg₀_pos
+    Polynomial.natDegree_add_eq_left_of_natDegree_lt
+      (by simpa [p, natDegree_C_mul (hδ_pos M).ne'] using hdeg₀)
   have hp_monic (M : ℕ) : (p M).Monic := by
     unfold Polynomial.Monic Polynomial.leadingCoeff
     rw [hp_deg]
@@ -210,9 +210,7 @@ protected lemma AffineFamily.isRealRooted_add_left_of_affine_family_of_natDegree
   have hsum_deg : (C t * f + g).natDegree = g.natDegree := by
     have hCt_deg : (C t * f).natDegree = f.natDegree := by rw [natDegree_C_mul ht.ne']
     exact
-      natDegree_add_eq_right_of_natDegree_lt_of_posLeadingCoeff
-        (by lia)
-        (hgnn.pos_leadingCoeff hg0)
+      Polynomial.natDegree_add_eq_right_of_natDegree_lt (by lia)
   apply AffineFamily.isRealRooted_of_add_C_mul_right_family_of_natDegree_le
   · intro s hs
     simpa [add_assoc, add_left_comm, add_comm, mul_assoc, left_distrib, right_distrib] using
@@ -276,7 +274,7 @@ private lemma isRealRooted_add_X_mul_right_of_affine_family
   have hCsXf_pos : HasPosLeadingCoeff (C s * (X * f)) :=
     hasPosLeadingCoeff_C_mul hs hXf_pos
   have hCsXf_nonneg : HasNonnegCoeffs (C s * (X * f)) :=
-    nonnegCoeffs_C_mul hs.le hfnn.X_mul
+    hasNonnegCoeffs_C_mul hs.le hfnn.X_mul
   have hbase_nonneg := hgnn.add hCsXf_nonneg
   have hbase_ne : g + C s * (X * f) ≠ 0 := by
     rw [add_comm]
@@ -285,17 +283,17 @@ private lemma isRealRooted_add_X_mul_right_of_affine_family
   have hbase_deg : f.natDegree ≤ (g + C s * (X * f)).natDegree := by
     rcases lt_trichotomy g.natDegree (X * f).natDegree with hdeg | hdeg | hdeg
     · have hsum_deg : (g + C s * (X * f)).natDegree = (C s * (X * f)).natDegree :=
-        natDegree_add_eq_right_of_natDegree_lt_of_posLeadingCoeff
-          (by simpa [natDegree_C_mul hs.ne'] using hdeg) hCsXf_pos
+        Polynomial.natDegree_add_eq_right_of_natDegree_lt
+          (by simpa [natDegree_C_mul hs.ne'] using hdeg)
       rw [hsum_deg, natDegree_C_mul hs.ne', natDegree_mul X_ne_zero hf0, natDegree_X]
       lia
     · have hsum_deg : (g + C s * (X * f)).natDegree = g.natDegree :=
         natDegree_add_eq_of_same_natDegree_of_posLeadingCoeff
           (by simpa [natDegree_C_mul hs.ne'] using hdeg) hg_pos hCsXf_pos
       simp_all
     · have hsum_deg : (g + C s * (X * f)).natDegree = g.natDegree :=
-        natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff
-          (by simpa [natDegree_C_mul hs.ne'] using hdeg) hg_pos
+        Polynomial.natDegree_add_eq_left_of_natDegree_lt
+          (by simpa [natDegree_C_mul hs.ne'] using hdeg)
       rw [hsum_deg]
       have hXf_deg : (X * f).natDegree = f.natDegree + 1 := by simp_all
       lia

RealRooted/AffineFamily/LowDegree.lean

@@ -63,7 +63,7 @@ private theorem not_degree_gap_ge_two_of_add_left_family_nonneg
     intro μ hμ
     have hbase := hfamily hμ
     have hbase_deg : (C μ * f + g).natDegree = g.natDegree := by
-      apply natDegree_add_eq_right_of_natDegree_lt_of_posLeadingCoeff _ hg_pos
+      apply Polynomial.natDegree_add_eq_right_of_natDegree_lt
       rw [natDegree_C_mul hμ.ne']
       lia
     have hn_lt : n < (C μ * f + g).natDegree := by lia
@@ -295,7 +295,7 @@ private lemma eval_nonpos_at_root_of_degree_one_of_affine_family
     nlinarith [sq_nonneg (2 * (s * a + A) * x + (a + B))]
   have hq_deg2 : q.natDegree = 2 := by rw [hq_eq]; exact natDegree_quadratic hquad_pos.ne'
   obtain ⟨x, hx_mem⟩ := Multiset.card_pos_iff_exists_mem.mp (show 0 < q.roots.card by
-    rw [card_roots_of_splits hq_rr.2, hq_deg2]
+    rw [Polynomial.splits_iff_card_roots.mp hq_rr.2, hq_deg2]
     lia)
   exact hq_noRoot x ((mem_roots hq_rr.1).mp hx_mem)
 

RealRooted/AffineFamily/Wronskian.lean

@@ -420,11 +420,11 @@ private lemma allComboRealRooted_of_affine_family_succDegree_not_isRoot_zero
     simp_all
   have hrs_len : rs.length = g.natDegree := by
     rw [show rs = g.roots.sort (· ≤ ·) by lia, Multiset.length_sort,
-      card_roots_of_splits hg_rr.2]
+      Polynomial.splits_iff_card_roots.mp hg_rr.2]
   have hus_eq : (↑us : Multiset ℝ) = f.roots := by
     apply Multiset.eq_of_le_of_card_le hus_sub
     calc
-      f.roots.card = f.natDegree := card_roots_of_splits hf_rr.2
+      f.roots.card = f.natDegree := Polynomial.splits_iff_card_roots.mp hf_rr.2
       _ = g.natDegree - 1 := by lia
       _ = rs.length - 1 := by lia
       _ = us.length := hus_len.symm
@@ -458,8 +458,8 @@ protected lemma AffineFamily.allComboRealRooted_of_affine_family_succDegree
       have hdeg_lt : f.natDegree < g.natDegree := by lia
       calc
         (g + f).natDegree = g.natDegree :=
-          natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff
-            hdeg_lt (hgnn.pos_leadingCoeff hg0)
+          Polynomial.natDegree_add_eq_left_of_natDegree_lt
+            hdeg_lt
         _ = f.natDegree + 1 := hsucc
     have hshift_aff :
         ∀ {s t : ℝ}, 0 < s → 0 < t →

RealRooted/AffineProperPosition.lean

@@ -322,18 +322,13 @@ theorem interl_affine_mul_X_self {s t : ℝ} (hs : 0 < s) :
     (isRealRooted_affine_factor hs).2).2
 
 theorem interl_affine_mul_X_add_X_affine_mul_X
-    {s t : ℝ} (hs : 0 < s) (ht : 0 < t) :
+    {s t : ℝ} (hs : 0 < s) :
     Interl ((C s * X + C t) * X + X) ((C s * X + C t) * X) := by
   rw [show ((C s * X + C t) * X + X : ℝ[X]) =
     X * (C s * X + C (t + 1)) by grind]
   rw [show ((C s * X + C t) * X : ℝ[X]) = X * (C s * X + C t) by ring]
-  have hleft_nonneg : HasNonnegCoeffs (C s * X + C t + 1 : ℝ[X]) := by
-    rw [show (C s * X + C t + 1 : ℝ[X]) = C s * X + C (t + 1) by grind]
-    exact hasNonnegCoeffs_affine_linear hs.le (by positivity)
   simpa [show (C s * X + C t + 1 : ℝ[X]) = C s * X + C (t + 1) by grind] using
-    (interl_affine_add_one_affine (t := t) hs).mul_X_both_of_nonneg
-      hleft_nonneg
-      (hasNonnegCoeffs_affine_linear (a := s) (b := t) hs.le ht.le)
+    (interl_affine_add_one_affine (t := t) hs).mul_X_both
 
 theorem interl_affine_mul_X_add_X_self {s t : ℝ} (hs : 0 < s) :
     Interl ((C s * X + C t) * X + X) ((C s * X + C t) * X + X) := by

RealRooted/AissenSchoenbergWhitney.lean

@@ -581,7 +581,7 @@ theorem aissenSchoenbergWhitney_reverse {p : ℝ[X]}
   · convert isPolyaFreqSeq_zero
     exact coeff_zero _
   · have hp_eq : p = C p.leadingCoeff * (p.roots.map fun r ↦ X - C r).prod :=
-      (C_leadingCoeff_mul_prod_multiset_X_sub_C (card_roots_of_splits hsplits)).symm
+      (C_leadingCoeff_mul_prod_multiset_X_sub_C (Polynomial.splits_iff_card_roots.mp hsplits)).symm
     rw [hp_eq]
     have hlc_nonneg : 0 ≤ p.leadingCoeff := (hpnn.pos_leadingCoeff hp0).le
     exact IsPolyaFreqSeq.const_mul p.leadingCoeff hlc_nonneg
@@ -599,7 +599,7 @@ theorem IsPolyaFreqSeq.of_forall_pos_add_C_mul_splits {p q : ℝ[X]}
     (a := p.coeff) (b := q.coeff) (by
       intro μ hμ
       have hnn : HasNonnegCoeffs (p + C μ * q) :=
-        hpnn.add (nonnegCoeffs_C_mul hμ.le hqnn)
+        hpnn.add (hasNonnegCoeffs_C_mul hμ.le hqnn)
       convert aissenSchoenbergWhitney_reverse hnn (hfamily hμ)
         (roots_nonpos_of_hasNonnegCoeffs hnn) using 1
       funext n

RealRooted/Applications/EulerianVariations/CyclicPathDescents.lean

@@ -160,7 +160,7 @@ theorem cyclicPathDescentPolynomial_simple_root_description
       exact hsimple.roots_nodup.notMem_erase hr
     exact lt_of_le_of_ne (hpf.roots_nonpos r hrRoot) hrne
   · rw [Multiset.card_erase_of_mem hzeroMem,
-      card_roots_of_splits hsplits,
+      Polynomial.splits_iff_card_roots.mp hsplits,
       natDegree_cyclicPathDescentPolynomial n hn]
     rfl
 

RealRooted/Applications/OEIS/A080721.lean

@@ -166,8 +166,8 @@ theorem legendre_strictInterl_polynomial (n : ℕ) :
     hasPosLeadingCoeff_add_of_natDegree_lt_left (by grind) haf_pos
   have hsum_deg :
       (a * legendre (n + 1) + b * legendre n).natDegree = n + 2 :=
-    (natDegree_add_eq_left_of_natDegree_lt_of_posLeadingCoeff
-      (by grind) haf_pos).trans hdeg_af
+    (Polynomial.natDegree_add_eq_left_of_natDegree_lt
+      (by grind)).trans hdeg_af
   have hb_nonpos :
       ∀ r : ℝ, (legendre (n + 1)).IsRoot r → b.eval r ≤ 0 := by
     intro r _

RealRooted/Applications/OEIS/A132885.lean

@@ -148,7 +148,7 @@ multiplicity.  They are distinct and strictly negative by
 `splits_simple_roots_neg`. -/
 theorem roots_card {n : ℕ} (hn : 2 ≤ n) :
     (polynomial n).roots.card = n / 2 := by
-  rw [card_roots_of_splits (splits_simple_roots_neg hn).1,
+  rw [Polynomial.splits_iff_card_roots.mp (splits_simple_roots_neg hn).1,
     natDegree_polynomial]
 
 end RealRooted.Applications.OEIS.A132885

RealRooted/Applications/OEIS/A144696/Endpoints.lean

@@ -131,7 +131,7 @@ private theorem a144696Polynomial_reciprocal_strictInterl_of_two_le
     loweringEulerStep_nonneg hEnn
       (generalizedEulerian_natDegree 1 n).le
   have hAnn : HasNonnegCoeffs (C 2 * E) :=
-    nonnegCoeffs_C_mul (by norm_num) hEnn
+    hasNonnegCoeffs_C_mul (by norm_num) hEnn
   have hpdeg : (C 2 * a144696Polynomial n).natDegree ≤ n := by
     rw [natDegree_C_mul (by norm_num), natDegree_a144696Polynomial]
   have hendpoint :

RealRooted/Applications/OEIS/A144696/StrictInterlacing.lean

@@ -197,7 +197,7 @@ theorem a144696Auxiliary_diagonal_interlaces
       simp
   have hroots_ne : f.roots ≠ 0 := by
     intro hzero
-    have hcard : f.roots.card = f.natDegree := card_roots_of_splits hsplitsF
+    have hcard : f.roots.card = f.natDegree := Polynomial.splits_iff_card_roots.mp hsplitsF
     rw [hzero] at hcard
     simp [hfdeg] at hcard
     lia

RealRooted/Applications/OEIS/A151775.lean

@@ -83,7 +83,7 @@ private theorem splits_splitFactorDerivative {a f : ℝ[X]}
     · exact absurd (pow_eq_zero_iff'.mp h).1 hf0
     · rw [h]; exact Splits.zero
   have hderivative : (derivative (a * f ^ m)).Splits :=
-    (eq_zero_or_splits_derivative (Or.inr (ha.mul (hf.pow m)))).resolve_left hD
+    (ha.mul (hf.pow m)).derivative
   exact Splits.of_dvd hderivative hD ⟨_, by rw [key, mul_comm]⟩
 
 private theorem splits_lowerStep {f : ℝ[X]} (hf : f.Splits) :