refactor(Algebra/Polynomial/Splits): continue deprecation (#32103)

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

Co-authored-by: tb65536 <[email protected]>

Author: tb65536

Mathlib/Algebra/CubicDiscriminant.lean

@@ -425,9 +425,9 @@ theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) :
 theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
     (map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z) := by
   rw [map_toPoly,
-    eq_prod_roots_of_splits <|
+    Splits.eq_prod_roots <|
       (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
-    leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
+    leadingCoeff_map, leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
   change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _
   rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
 

Mathlib/Algebra/Polynomial/Factors.lean

@@ -92,6 +92,33 @@ theorem splits_of_degree_le_zero {f : R[X]} (hf : degree f ≤ 0) :
     Splits f :=
   splits_of_natDegree_eq_zero (natDegree_eq_zero_iff_degree_le_zero.mpr hf)
 
+theorem _root_.IsUnit.splits [NoZeroDivisors R] {f : R[X]} (hf : IsUnit f) : Splits f :=
+  splits_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hf)
+
+@[deprecated (since := "2025-11-27")]
+alias splits_of_isUnit := IsUnit.splits
+
+theorem splits_of_natDegree_le_one_of_invertible {f : R[X]}
+    (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits := by
+  obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf
+  rcases eq_or_ne a 0 with rfl | ha
+  · simp
+  · replace h : Invertible a := by simpa [leadingCoeff, ha] using h
+    rw [← mul_invOf_cancel_left a b, C_mul, ← mul_add]
+    exact (Splits.C a).mul (Splits.X_add_C _)
+
+theorem splits_of_degree_le_one_of_invertible {f : R[X]}
+    (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits :=
+  splits_of_natDegree_le_one_of_invertible (natDegree_le_of_degree_le hf) h
+
+theorem splits_of_natDegree_le_one_of_monic {f : R[X]} (hf : f.natDegree ≤ 1) (h : Monic f) :
+    f.Splits :=
+  splits_of_natDegree_le_one_of_invertible hf (h.leadingCoeff ▸ invertibleOne)
+
+theorem splits_of_degree_le_one_of_monic {f : R[X]} (hf : f.degree ≤ 1) (h : Monic f) :
+    f.Splits :=
+  splits_of_natDegree_le_one_of_monic (natDegree_le_of_degree_le hf) h
+
 end Semiring
 
 section CommSemiring
@@ -146,6 +173,35 @@ theorem Splits.natDegree_le_one_of_irreducible {f : R[X]} (hf : Splits f)
     grw [hm, this, natDegree_mul_le]
     simp
 
+theorem Splits.comp_of_natDegree_le_one_of_invertible {f g : R[X]} (hf : f.Splits)
+    (hg : g.natDegree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits := by
+  rcases lt_or_eq_of_le hg with hg | hg
+  · rw [eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)]
+    simp
+  obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hf
+  rw [hm, mul_comp, C_comp, multiset_prod_comp]
+  refine (Splits.C _).mul (multisetProd ?_)
+  simp only [Multiset.mem_map]
+  rintro - ⟨-, ⟨a, -, rfl⟩, rfl⟩
+  apply splits_of_natDegree_le_one_of_invertible (by simpa)
+  rw [leadingCoeff, hg] at h
+  simpa [leadingCoeff, hg]
+
+theorem Splits.comp_of_degree_le_one_of_invertible {f g : R[X]} (hf : f.Splits)
+    (hg : g.degree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits :=
+  hf.comp_of_natDegree_le_one_of_invertible (natDegree_le_of_degree_le hg) h
+
+theorem Splits.comp_of_natDegree_le_one_of_monic {f g : R[X]} (hf : f.Splits)
+    (hg : g.natDegree ≤ 1) (h : Monic g) : (f.comp g).Splits :=
+  hf.comp_of_natDegree_le_one_of_invertible hg (h.leadingCoeff ▸ invertibleOne)
+
+theorem Splits.comp_of_degree_le_one_of_monic {f g : R[X]} (hf : f.Splits)
+    (hg : g.degree ≤ 1) (h : Monic g) : (f.comp g).Splits :=
+  hf.comp_of_natDegree_le_one_of_monic (natDegree_le_of_degree_le hg) h
+
+theorem Splits.comp_X_add_C {f : R[X]} (hf : f.Splits) (a : R) : (f.comp (X + C a)).Splits :=
+  hf.comp_of_natDegree_le_one_of_monic (natDegree_add_C.trans_le natDegree_X_le) (monic_X_add_C a)
+
 end CommSemiring
 
 section Ring
@@ -195,6 +251,9 @@ theorem Splits.exists_eval_eq_zero (hf : Splits f) (hf0 : degree f ≠ 0) :
   obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha
   exact ⟨a, hm ▸ by simp⟩
 
+theorem Splits.comp_X_sub_C {f : R[X]} (hf : f.Splits) (a : R) : (f.comp (X - C a)).Splits :=
+  hf.comp_of_natDegree_le_one_of_monic (natDegree_sub_C.trans_le natDegree_X_le) (monic_X_sub_C a)
+
 variable [IsDomain R]
 
 theorem Splits.eq_prod_roots (hf : Splits f) :
@@ -249,15 +308,18 @@ theorem splits_mul_iff (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) :
     have := ih (by aesop) hg₀ (f * g) rfl  (splits_X_sub_C_mul_iff.mp h) hn
     aesop
 
-theorem Splits.of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
+theorem Splits.splits_of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
   obtain ⟨g, rfl⟩ := hfg
   exact ((splits_mul_iff (by aesop) (by aesop)).mp hg).1
 
+@[deprecated (since := "2025-11-27")]
+alias Splits.of_dvd := Splits.splits_of_dvd
+
 -- Todo: Remove or fix name once `Splits` is gone.
 theorem Splits.splits (hf : Splits f) :
     f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g ≤ 1 :=
   or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
-    (hf.of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
+    (hf.splits_of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
 
 lemma map_sub_sprod_roots_eq_prod_map_eval
     (s : Multiset R) (g : R[X]) (hg : g.Monic) (hg' : g.Splits) :
@@ -304,6 +366,33 @@ section Field
 
 variable [Field R]
 
+theorem Splits.comp_of_natDegree_le_one {f g : R[X]} (hf : f.Splits) (hg : g.natDegree ≤ 1) :
+    (f.comp g).Splits := by
+  rcases eq_or_ne g 0 with rfl | hg0
+  · simp
+  · exact Splits.comp_of_natDegree_le_one_of_invertible hf hg
+      (invertibleOfNonzero (leadingCoeff_ne_zero.mpr hg0))
+
+theorem Splits.comp_of_degree_le_one {f g : R[X]} (hf : f.Splits) (hg : g.degree ≤ 1) :
+    (f.comp g).Splits :=
+  hf.comp_of_natDegree_le_one (natDegree_le_of_degree_le hg)
+
+theorem splits_iff_comp_splits_of_natDegree_eq_one {f g : R[X]} (hg : g.natDegree = 1) :
+    f.Splits ↔ (f.comp g).Splits := by
+  refine ⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩
+  obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hg.le
+  have ha : a ≠ 0 := by contrapose! hg; simp [hg]
+  have : f = (f.comp (C a * X + C b)).comp ((C a⁻¹ * (X - C b))) := by
+    simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]
+    rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
+  rw [this]
+  refine Splits.comp_of_natDegree_le_one hf ?_
+  rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]
+
+theorem splits_iff_comp_splits_of_degree_eq_one {f g : R[X]} (hg : g.degree = 1) :
+    f.Splits ↔ (f.comp g).Splits :=
+  splits_iff_comp_splits_of_natDegree_eq_one (natDegree_eq_of_degree_eq_some hg)
+
 open UniqueFactorizationMonoid in
 -- Todo: Remove or fix name.
 theorem splits_iff_splits {f : R[X]} :
@@ -317,8 +406,7 @@ theorem splits_iff_splits {f : R[X]} :
   · simp [hf0]
   obtain ⟨u, hu⟩ := factors_prod hf0
   rw [← hu]
-  refine (Splits.multisetProd fun g hg ↦ ?_).mul
-    (splits_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit u.isUnit))
+  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
   exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
 
 end Field

Mathlib/Algebra/Polynomial/Splits.lean

@@ -66,14 +66,11 @@ alias splits_of_natDegree_le_one := Splits.of_natDegree_le_one
 @[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
-  simp [hf.mul hg]
+@[deprecated (since := "2025-11-25")]
+alias splits_mul := Splits.mul
 
-theorem splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Splits ((f * g).map i)) :
-    Splits (f.map i) ∧ Splits (g.map i) := by
-  simp only [Splits, Polynomial.map_mul, mul_ne_zero_iff] at hfg h
-  exact (splits_mul_iff hfg.1 hfg.2).mp h
+@[deprecated (since := "2025-11-25")]
+alias splits_of_splits_mul' := splits_mul_iff
 
 @[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]} :
@@ -83,9 +80,6 @@ theorem splits_map_iff {L : Type*} [CommRing L] (i : K →+* L) (j : L →+* F)
 @[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 _
-
 @[deprecated (since := "2025-11-24")]
 alias splits_X_sub_C := Splits.X_sub_C
 
@@ -108,43 +102,9 @@ theorem splits_id_iff_splits {f : K[X]} :
 
 variable {i}
 
-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")]
+@[deprecated (since := "2025-11-25")]
 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 : 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 [invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
-      ← mul_assoc]
-    simp
-  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 : 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 : 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
-
 variable (i)
 
 theorem exists_root_of_splits' {f : K[X]} (hs : Splits (f.map i)) (hf0 : degree (f.map i) ≠ 0) :
@@ -194,22 +154,19 @@ theorem Splits.def {i : K →+* L} {f : K[X]} (h : Splits (f.map i)) :
     f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 :=
   (splits_iff i f).mp h
 
-theorem splits_of_splits_mul {f g : K[X]} (hfg : f * g ≠ 0) (h : Splits ((f * g).map i)) :
-    Splits (f.map i) ∧ Splits (g.map i) :=
-  splits_of_splits_mul' i (map_ne_zero hfg) h
+@[deprecated (since := "2025-11-25")]
+alias splits_of_splits_mul := splits_mul_iff
 
-theorem splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits (f.map i)) (hgf : g ∣ f) :
-    Splits (g.map i) := by
-  obtain ⟨f, rfl⟩ := hgf
-  exact (splits_of_splits_mul i hf0 hf).1
+@[deprecated (since := "2025-11-25")]
+alias splits_of_splits_of_dvd := Splits.splits_of_dvd
 
 theorem splits_of_splits_gcd_left [DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0)
     (hf : Splits (f.map i)) : Splits ((EuclideanDomain.gcd f g).map i) :=
-  Polynomial.splits_of_splits_of_dvd i hf0 hf (EuclideanDomain.gcd_dvd_left f g)
+  Splits.splits_of_dvd hf (map_ne_zero hf0) <| map_dvd i <| EuclideanDomain.gcd_dvd_left f g
 
 theorem splits_of_splits_gcd_right [DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0)
     (hg : Splits (g.map i)) : Splits ((EuclideanDomain.gcd f g).map i) :=
-  Polynomial.splits_of_splits_of_dvd i hg0 hg (EuclideanDomain.gcd_dvd_right f g)
+  Splits.splits_of_dvd hg (map_ne_zero hg0) <| map_dvd i <| EuclideanDomain.gcd_dvd_right f g
 
 theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
     (∀ j ∈ t, s j ≠ 0) → (((∏ x ∈ t, s x).map i).Splits ↔ ∀ j ∈ t, ((s j).map i).Splits) := by
@@ -286,19 +243,15 @@ theorem adjoin_rootSet_eq_range [Algebra R K] [Algebra R L] {p : R[X]}
   rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
   exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff
 
-theorem eq_prod_roots_of_splits {p : K[X]} {i : K →+* L} (hsplit : Splits (p.map i)) :
-    p.map i = C (i p.leadingCoeff) * ((p.map i).roots.map fun a => X - C a).prod := by
-  rw [← leadingCoeff_map]; symm
-  apply C_leadingCoeff_mul_prod_multiset_X_sub_C
-  rw [natDegree_map]; exact (natDegree_eq_card_roots hsplit).symm
+@[deprecated (since := "2025-11-25")]
+alias eq_prod_roots_of_splits := Splits.eq_prod_roots
 
-theorem eq_prod_roots_of_splits_id {p : K[X]} (hsplit : Splits p) :
-    p = C p.leadingCoeff * (p.roots.map fun a => X - C a).prod :=
-  hsplit.eq_prod_roots
+@[deprecated (since := "2025-11-25")]
+alias eq_prod_roots_of_splits_id := Splits.eq_prod_roots
 
 theorem Splits.dvd_of_roots_le_roots {p q : K[X]} (hp : p.Splits) (hp0 : p ≠ 0)
     (hq : p.roots ≤ q.roots) : p ∣ q := by
-  rw [eq_prod_roots_of_splits_id hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
+  rw [Splits.eq_prod_roots hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
   exact dvd_trans
     (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq))
     (prod_multiset_X_sub_C_dvd _)
@@ -311,7 +264,7 @@ theorem Splits.dvd_iff_roots_le_roots {p q : K[X]}
 theorem aeval_eq_prod_aroots_sub_of_splits [Algebra K L] {p : K[X]}
     (hsplit : Splits (p.map (algebraMap K L))) (v : L) :
     aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod := by
-  rw [← eval_map_algebraMap, eq_prod_roots_of_splits hsplit]
+  rw [← eval_map_algebraMap, Splits.eq_prod_roots hsplit]
   simp [eval_multiset_prod]
 
 theorem eval_eq_prod_roots_sub_of_splits_id {p : K[X]}
@@ -322,7 +275,7 @@ theorem eval_eq_prod_roots_sub_of_splits_id {p : K[X]}
 
 theorem eq_prod_roots_of_monic_of_splits_id {p : K[X]} (m : Monic p)
     (hsplit : Splits p) : p = (p.roots.map fun a => X - C a).prod := by
-  convert eq_prod_roots_of_splits_id hsplit
+  convert Splits.eq_prod_roots hsplit
   simp [m]
 
 theorem aeval_eq_prod_aroots_sub_of_monic_of_splits [Algebra K L] {p : K[X]} (m : Monic p)
@@ -338,7 +291,7 @@ theorem eval_eq_prod_roots_sub_of_monic_of_splits_id {p : K[X]} (m : Monic p)
 theorem eq_X_sub_C_of_splits_of_single_root {x : K} {h : K[X]} (h_splits : Splits (h.map i))
     (h_roots : (h.map i).roots = {i x}) : h = C h.leadingCoeff * (X - C x) := by
   apply Polynomial.map_injective _ i.injective
-  rw [eq_prod_roots_of_splits h_splits, h_roots]
+  rw [Splits.eq_prod_roots h_splits, h_roots]
   simp
 
 variable (R) in
@@ -389,7 +342,7 @@ theorem splits_of_comp (j : L →+* F) {f : K[X]} (h : Splits (f.map (j.comp i))
   choose lift lift_eq using roots_mem_range
   rw [splits_iff_exists_multiset]
   refine ⟨(f.map (j.comp i)).roots.pmap lift fun _ ↦ id, map_injective _ j.injective ?_⟩
-  conv_lhs => rw [Polynomial.map_map, eq_prod_roots_of_splits h]
+  conv_lhs => rw [Polynomial.map_map, Splits.eq_prod_roots h]
   simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub,
     map_C, map_X, lift_eq, Multiset.pmap_eq_map]
   simp
@@ -428,7 +381,7 @@ theorem eval₂_derivative_of_splits [DecidableEq L] {P : K[X]} {f : K →+* L}
     (x : L) :
     eval₂ f x P.derivative = f (P.leadingCoeff) *
       ((P.map f).roots.map fun a ↦ (((P.map f).roots.erase a).map (x - ·)).prod).sum := by
-  conv_lhs => rw [← eval_map, ← derivative_map, eq_prod_roots_of_splits hP]
+  conv_lhs => rw [← eval_map, ← derivative_map, Splits.eq_prod_roots hP]
   classical
   simp [derivative_prod, eval_multisetSum, eval_multiset_prod]
 
@@ -460,7 +413,7 @@ theorem eval_derivative_eq_eval_mul_sum_of_splits {p : K[X]} {x : K}
   classical
   suffices p.roots.map (fun z ↦ p.leadingCoeff * ((p.roots.erase z).map (fun w ↦ x - w) ).prod) =
       p.roots.map fun i ↦ p.leadingCoeff * ((x - i)⁻¹ * (p.roots.map (fun z ↦ x - z)).prod) by
-    nth_rw 2 [p.eq_prod_roots_of_splits_id h]
+    nth_rw 2 [Splits.eq_prod_roots h]
     simp [eval_derivative_of_splits h, ← Multiset.sum_map_mul_left, this, eval_multiset_prod,
       mul_comm, mul_left_comm]
   refine Multiset.map_congr rfl fun z hz ↦ ?_
@@ -488,7 +441,7 @@ theorem coeff_zero_eq_prod_roots_of_monic_of_splits {P : K[X]} (hmo : P.Monic)
 
 theorem nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits {P : K[X]}
     (hP : P.Splits) : P.nextCoeff = -P.leadingCoeff * P.roots.sum := by
-  nth_rw 1 [eq_prod_roots_of_splits_id hP]
+  nth_rw 1 [Splits.eq_prod_roots hP]
   simp [Multiset.sum_map_neg', monic_X_sub_C, Monic.nextCoeff_multiset_prod]
 
 /-- If `P` is a monic polynomial that splits, then `P.nextCoeff` equals the negative of the sum

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

@@ -209,7 +209,7 @@ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p.
   by_cases hp : p = 0
   · simp [hp]
   have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map]
-  nth_rw 1 [eq_prod_roots_of_splits_id (IsAlgClosed.splits p)]
+  nth_rw 1 [(IsAlgClosed.splits p).eq_prod_roots]
   rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [hp, X_sub_C_ne_zero])]
   simp [posLog_eq_log_max_one, logMahlerMeasure_eq_log_MahlerMeasure,
     prod_mahlerMeasure_eq_mahlerMeasure_prod, log_multiset_prod this]

Mathlib/FieldTheory/AbelRuffini.lean

@@ -151,8 +151,8 @@ theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [F
     rw [hb', zero_pow hn] at hb
     exact ha' hb.symm
   let s := ((X ^ n - C a).map i).roots
-  have hs : _ = _ * (s.map _).prod := eq_prod_roots_of_splits h
-  rw [leadingCoeff_X_pow_sub_C hn', map_one, C_1, one_mul] at hs
+  have hs : _ = _ * (s.map _).prod := h.eq_prod_roots
+  rw [leadingCoeff_map, leadingCoeff_X_pow_sub_C hn', RingHom.map_one, C_1, one_mul] at hs
   have hs' : Multiset.card s = n := (natDegree_eq_card_roots h).symm.trans natDegree_X_pow_sub_C
   apply @splits_of_exists_multiset F E _ _ i (X ^ n - 1) (s.map fun c : E => c / b)
   rw [leadingCoeff_X_pow_sub_one hn', map_one, C_1, one_mul, Multiset.map_map]
@@ -282,8 +282,8 @@ theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (
     · exact minpoly.ne_zero (isIntegral (α ^ n)) h'
     · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
   apply gal_isSolvable_of_splits
-  · exact ⟨splits_of_splits_of_dvd _ hp (SplittingField.splits (p.comp (X ^ n)))
-      (minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval]))⟩
+  · exact ⟨(SplittingField.splits (p.comp (X ^ n))).splits_of_dvd (map_ne_zero hp)
+      ((map_dvd_map' _).mpr (minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval])))⟩
   · refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
     · exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])
     · obtain ⟨s, hs⟩ := splits_iff_exists_multiset.1 (SplittingField.splits p)
@@ -305,9 +305,9 @@ open IntermediateField
 theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ := by
   let p := minpoly F α
   let q := minpoly F β
-  have hpq := Polynomial.splits_of_splits_mul _
-    (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
-    (SplittingField.splits (p * q))
+  have hpq := SplittingField.splits (p * q)
+  rw [Polynomial.map_mul, splits_mul_iff (map_ne_zero (minpoly.ne_zero (isIntegral α)))
+    (map_ne_zero (minpoly.ne_zero (isIntegral β)))] at hpq
   let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField :=
     Classical.choice <| nonempty_algHom_adjoin_of_splits <| by
       intro x hx