diff --git a/Mathbin/Algebra/Polynomial/GroupRingAction.lean b/Mathbin/Algebra/Polynomial/GroupRingAction.lean
index 5d66e70bb4..2d0df8c6b3 100644
--- a/Mathbin/Algebra/Polynomial/GroupRingAction.lean
+++ b/Mathbin/Algebra/Polynomial/GroupRingAction.lean
@@ -102,7 +102,7 @@ noncomputable def prodXSubSmul (x : R) : R[X] :=
 #align prod_X_sub_smul prodXSubSmul
 
 theorem prodXSubSmul.monic (x : R) : (prodXSubSmul G R x).Monic :=
-  Polynomial.monic_prod_of_monic _ _ fun g _ => Polynomial.monic_x_sub_c _
+  Polynomial.monic_prod_of_monic _ _ fun g _ => Polynomial.monic_X_sub_C _
 #align prod_X_sub_smul.monic prodXSubSmul.monic
 
 theorem prodXSubSmul.eval (x : R) : (prodXSubSmul G R x).eval x = 0 :=
diff --git a/Mathbin/Data/Polynomial/Div.lean b/Mathbin/Data/Polynomial/Div.lean
index 44f2de7c14..1c1334cca4 100644
--- a/Mathbin/Data/Polynomial/Div.lean
+++ b/Mathbin/Data/Polynomial/Div.lean
@@ -564,7 +564,7 @@ def rootMultiplicity (a : R) (p : R[X]) : ℕ :=
   if h0 : p = 0 then 0
   else
     let I : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
-      @Not.decidable _ (decidableDvdMonic p ((monic_x_sub_c a).pow (n + 1)))
+      @Not.decidable _ (decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1)))
     Nat.find (multiplicity_X_sub_C_finite a h0)
 #align polynomial.root_multiplicity Polynomial.rootMultiplicity
 
@@ -614,7 +614,7 @@ theorem pow_rootMultiplicity_dvd (p : R[X]) (a : R) : (X - C a) ^ rootMultiplici
 theorem divByMonic_mul_pow_rootMultiplicity_eq (p : R[X]) (a : R) :
     p /ₘ (X - C a) ^ rootMultiplicity a p * (X - C a) ^ rootMultiplicity a p = p :=
   by
-  have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_x_sub_c _).pow _
+  have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
   conv_rhs =>
       rw [← mod_by_monic_add_div p this,
         (dvd_iff_mod_by_monic_eq_zero this).2 (pow_root_multiplicity_dvd _ _)] <;>
diff --git a/Mathbin/Data/Polynomial/FieldDivision.lean b/Mathbin/Data/Polynomial/FieldDivision.lean
index 5a7296d380..d3f85bc6c4 100644
--- a/Mathbin/Data/Polynomial/FieldDivision.lean
+++ b/Mathbin/Data/Polynomial/FieldDivision.lean
@@ -215,11 +215,11 @@ theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
 #align polynomial.div_by_monic_eq_div Polynomial.divByMonic_eq_div
 
 theorem mod_x_sub_c_eq_c_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=
-  modByMonic_eq_mod p (monic_x_sub_c a) ▸ modByMonic_x_sub_c_eq_c_eval _ _
+  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_x_sub_c_eq_c_eval _ _
 #align polynomial.mod_X_sub_C_eq_C_eval Polynomial.mod_x_sub_c_eq_c_eval
 
 theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=
-  divByMonic_eq_div p (monic_x_sub_c a) ▸ mul_divByMonic_eq_iff_isRoot
+  divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot
 #align polynomial.mul_div_eq_iff_is_root Polynomial.mul_div_eq_iff_isRoot
 
 instance : EuclideanDomain R[X] :=
diff --git a/Mathbin/Data/Polynomial/Monic.lean b/Mathbin/Data/Polynomial/Monic.lean
index aa767f95d2..994ad6892a 100644
--- a/Mathbin/Data/Polynomial/Monic.lean
+++ b/Mathbin/Data/Polynomial/Monic.lean
@@ -35,14 +35,23 @@ section Semiring
 
 variable [Semiring R] {p q r : R[X]}
 
+#print Polynomial.monic_zero_iff_subsingleton /-
 theorem monic_zero_iff_subsingleton : Monic (0 : R[X]) ↔ Subsingleton R :=
   subsingleton_iff_zero_eq_one
 #align polynomial.monic_zero_iff_subsingleton Polynomial.monic_zero_iff_subsingleton
+-/
 
+/- warning: polynomial.not_monic_zero_iff -> Polynomial.not_monic_zero_iff is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R], Iff (Not (Polynomial.Monic.{u1} R _inst_1 (OfNat.ofNat.{u1} (Polynomial.{u1} R _inst_1) 0 (OfNat.mk.{u1} (Polynomial.{u1} R _inst_1) 0 (Zero.zero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.zero.{u1} R _inst_1)))))) (Ne.{succ u1} R (OfNat.ofNat.{u1} R 0 (OfNat.mk.{u1} R 0 (Zero.zero.{u1} R (MulZeroClass.toHasZero.{u1} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))))) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))))))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R], Iff (Not (Polynomial.Monic.{u1} R _inst_1 (OfNat.ofNat.{u1} (Polynomial.{u1} R _inst_1) 0 (Zero.toOfNat0.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.zero.{u1} R _inst_1))))) (Ne.{succ u1} R (OfNat.ofNat.{u1} R 0 (Zero.toOfNat0.{u1} R (MonoidWithZero.toZero.{u1} R (Semiring.toMonoidWithZero.{u1} R _inst_1)))) (OfNat.ofNat.{u1} R 1 (One.toOfNat1.{u1} R (Semiring.toOne.{u1} R _inst_1))))
+Case conversion may be inaccurate. Consider using '#align polynomial.not_monic_zero_iff Polynomial.not_monic_zero_iffₓ'. -/
 theorem not_monic_zero_iff : ¬Monic (0 : R[X]) ↔ (0 : R) ≠ 1 :=
   (monic_zero_iff_subsingleton.trans subsingleton_iff_zero_eq_one.symm).Not
 #align polynomial.not_monic_zero_iff Polynomial.not_monic_zero_iff
 
+#print Polynomial.monic_zero_iff_subsingleton' /-
 theorem monic_zero_iff_subsingleton' :
     Monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ ∀ a b : R, a = b :=
   Polynomial.monic_zero_iff_subsingleton.trans
@@ -50,7 +59,14 @@ theorem monic_zero_iff_subsingleton' :
       intro
       simp, fun h => subsingleton_iff.mpr h.2⟩
 #align polynomial.monic_zero_iff_subsingleton' Polynomial.monic_zero_iff_subsingleton'
+-/
 
+/- warning: polynomial.monic.as_sum -> Polynomial.Monic.as_sum is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u1} R _inst_1 p) -> (Eq.{succ u1} (Polynomial.{u1} R _inst_1) p (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (Polynomial.X.{u1} R _inst_1) (Polynomial.natDegree.{u1} R _inst_1 p)) (Finset.sum.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (Finset.range (Polynomial.natDegree.{u1} R _inst_1 p)) (fun (i : Nat) => HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) => R -> (Polynomial.{u1} R _inst_1)) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (Polynomial.C.{u1} R _inst_1) (Polynomial.coeff.{u1} R _inst_1 p i)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (Polynomial.X.{u1} R _inst_1) i)))))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u1} R _inst_1 p) -> (Eq.{succ u1} (Polynomial.{u1} R _inst_1) p (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (Polynomial.X.{u1} R _inst_1) (Polynomial.natDegree.{u1} R _inst_1 p)) (Finset.sum.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (Finset.range (Polynomial.natDegree.{u1} R _inst_1 p)) (fun (i : Nat) => HMul.hMul.{u1, u1, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) (Polynomial.coeff.{u1} R _inst_1 p i)) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) (Polynomial.coeff.{u1} R _inst_1 p i)) (Polynomial.mul'.{u1} R _inst_1)) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))))) (Polynomial.C.{u1} R _inst_1) (Polynomial.coeff.{u1} R _inst_1 p i)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (Polynomial.X.{u1} R _inst_1) i)))))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic.as_sum Polynomial.Monic.as_sumₓ'. -/
 theorem Monic.as_sum (hp : p.Monic) :
     p = X ^ p.natDegree + ∑ i in range p.natDegree, C (p.coeff i) * X ^ i :=
   by
@@ -59,6 +75,7 @@ theorem Monic.as_sum (hp : p.Monic) :
   exact congr_arg C hp
 #align polynomial.monic.as_sum Polynomial.Monic.as_sum
 
+#print Polynomial.ne_zero_of_ne_zero_of_monic /-
 theorem ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : Monic q) : q ≠ 0 :=
   by
   rintro rfl
@@ -66,7 +83,9 @@ theorem ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : Monic q) : q ≠ 0 :=
   rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp
   exact hp rfl
 #align polynomial.ne_zero_of_ne_zero_of_monic Polynomial.ne_zero_of_ne_zero_of_monic
+-/
 
+#print Polynomial.Monic.map /-
 theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f) :=
   by
   nontriviality
@@ -78,37 +97,61 @@ theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f)
   suffices p.coeff (map f p).natDegree = 1 by simp [this]
   rwa [nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f this)]
 #align polynomial.monic.map Polynomial.Monic.map
+-/
 
-theorem monic_c_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) :
+/- warning: polynomial.monic_C_mul_of_mul_leading_coeff_eq_one -> Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {b : R}, (Eq.{succ u1} R (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (Distrib.toHasMul.{u1} R (NonUnitalNonAssocSemiring.toDistrib.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) b (Polynomial.leadingCoeff.{u1} R _inst_1 p)) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))))) -> (Polynomial.Monic.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) => R -> (Polynomial.{u1} R _inst_1)) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (Polynomial.C.{u1} R _inst_1) b) p))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {b : R}, (Eq.{succ u1} R (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) b (Polynomial.leadingCoeff.{u1} R _inst_1 p)) (OfNat.ofNat.{u1} R 1 (One.toOfNat1.{u1} R (Semiring.toOne.{u1} R _inst_1)))) -> (Polynomial.Monic.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) b) (Polynomial.{u1} R _inst_1) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) b) (instHMul.{u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) b) (Polynomial.mul'.{u1} R _inst_1)) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))))) (Polynomial.C.{u1} R _inst_1) b) p))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_C_mul_of_mul_leading_coeff_eq_one Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_oneₓ'. -/
+theorem monic_C_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) :
     Monic (C b * p) := by
   nontriviality
   rw [monic, leading_coeff_mul' _] <;> simp [leading_coeff_C b, hp]
-#align polynomial.monic_C_mul_of_mul_leading_coeff_eq_one Polynomial.monic_c_mul_of_mul_leadingCoeff_eq_one
-
-theorem monic_mul_c_of_leadingCoeff_mul_eq_one {b : R} (hp : p.leadingCoeff * b = 1) :
+#align polynomial.monic_C_mul_of_mul_leading_coeff_eq_one Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one
+
+/- warning: polynomial.monic_mul_C_of_leading_coeff_mul_eq_one -> Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {b : R}, (Eq.{succ u1} R (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (Distrib.toHasMul.{u1} R (NonUnitalNonAssocSemiring.toDistrib.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (Polynomial.leadingCoeff.{u1} R _inst_1 p) b) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))))) -> (Polynomial.Monic.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) p (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) => R -> (Polynomial.{u1} R _inst_1)) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (Polynomial.C.{u1} R _inst_1) b)))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {b : R}, (Eq.{succ u1} R (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) (Polynomial.leadingCoeff.{u1} R _inst_1 p) b) (OfNat.ofNat.{u1} R 1 (One.toOfNat1.{u1} R (Semiring.toOne.{u1} R _inst_1)))) -> (Polynomial.Monic.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) b) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) p (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))))) (Polynomial.C.{u1} R _inst_1) b)))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_mul_C_of_leading_coeff_mul_eq_one Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_oneₓ'. -/
+theorem monic_mul_C_of_leadingCoeff_mul_eq_one {b : R} (hp : p.leadingCoeff * b = 1) :
     Monic (p * C b) := by
   nontriviality
   rw [monic, leading_coeff_mul' _] <;> simp [leading_coeff_C b, hp]
-#align polynomial.monic_mul_C_of_leading_coeff_mul_eq_one Polynomial.monic_mul_c_of_leadingCoeff_mul_eq_one
+#align polynomial.monic_mul_C_of_leading_coeff_mul_eq_one Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
 
+#print Polynomial.monic_of_degree_le /-
 theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : Monic p :=
   Decidable.byCases
     (fun H : degree p < n => eq_of_zero_eq_one (H2 ▸ (coeff_eq_zero_of_degree_lt H).symm) _ _)
     fun H : ¬degree p < n => by
     rwa [monic, leading_coeff, nat_degree, (lt_or_eq_of_le H1).resolve_left H]
 #align polynomial.monic_of_degree_le Polynomial.monic_of_degree_le
+-/
 
-theorem monic_x_pow_add {n : ℕ} (H : degree p ≤ n) : Monic (X ^ (n + 1) + p) :=
+#print Polynomial.monic_X_pow_add /-
+theorem monic_X_pow_add {n : ℕ} (H : degree p ≤ n) : Monic (X ^ (n + 1) + p) :=
   have H1 : degree p < n + 1 := lt_of_le_of_lt H (WithBot.coe_lt_coe.2 (Nat.lt_succ_self n))
   monic_of_degree_le (n + 1)
     (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H1)))
     (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero])
-#align polynomial.monic_X_pow_add Polynomial.monic_x_pow_add
-
-theorem monic_x_add_c (x : R) : Monic (X + C x) :=
-  pow_one (X : R[X]) ▸ monic_x_pow_add degree_C_le
-#align polynomial.monic_X_add_C Polynomial.monic_x_add_c
+#align polynomial.monic_X_pow_add Polynomial.monic_X_pow_add
+-/
 
+/- warning: polynomial.monic_X_add_C -> Polynomial.monic_X_add_C is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] (x : R), Polynomial.Monic.{u1} R _inst_1 (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (Polynomial.X.{u1} R _inst_1) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) => R -> (Polynomial.{u1} R _inst_1)) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (Polynomial.C.{u1} R _inst_1) x))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] (x : R), Polynomial.Monic.{u1} R _inst_1 (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) x) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (Polynomial.X.{u1} R _inst_1) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))))) (Polynomial.C.{u1} R _inst_1) x))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_X_add_C Polynomial.monic_X_add_Cₓ'. -/
+theorem monic_X_add_C (x : R) : Monic (X + C x) :=
+  pow_one (X : R[X]) ▸ monic_X_pow_add degree_C_le
+#align polynomial.monic_X_add_C Polynomial.monic_X_add_C
+
+#print Polynomial.Monic.mul /-
 theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=
   if h0 : (0 : R) = 1 then
     haveI := subsingleton_of_zero_eq_one h0
@@ -119,38 +162,50 @@ theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=
       simp [monic.def.1 hp, monic.def.1 hq, Ne.symm h0]
     rw [monic.def, leading_coeff_mul' this, monic.def.1 hp, monic.def.1 hq, one_mul]
 #align polynomial.monic.mul Polynomial.Monic.mul
+-/
 
+#print Polynomial.Monic.pow /-
 theorem Monic.pow (hp : Monic p) : ∀ n : ℕ, Monic (p ^ n)
   | 0 => monic_one
   | n + 1 => by
     rw [pow_succ]
     exact hp.mul (monic.pow n)
 #align polynomial.monic.pow Polynomial.Monic.pow
+-/
 
+#print Polynomial.Monic.add_of_left /-
 theorem Monic.add_of_left (hp : Monic p) (hpq : degree q < degree p) : Monic (p + q) := by
   rwa [monic, add_comm, leading_coeff_add_of_degree_lt hpq]
 #align polynomial.monic.add_of_left Polynomial.Monic.add_of_left
+-/
 
+#print Polynomial.Monic.add_of_right /-
 theorem Monic.add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p + q) := by
   rwa [monic, leading_coeff_add_of_degree_lt hpq]
 #align polynomial.monic.add_of_right Polynomial.Monic.add_of_right
+-/
 
+#print Polynomial.Monic.of_mul_monic_left /-
 theorem Monic.of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic :=
   by
   contrapose! hpq
   rw [monic.def] at hpq⊢
   rwa [leading_coeff_monic_mul hp]
 #align polynomial.monic.of_mul_monic_left Polynomial.Monic.of_mul_monic_left
+-/
 
+#print Polynomial.Monic.of_mul_monic_right /-
 theorem Monic.of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic :=
   by
   contrapose! hpq
   rw [monic.def] at hpq⊢
   rwa [leading_coeff_mul_monic hq]
 #align polynomial.monic.of_mul_monic_right Polynomial.Monic.of_mul_monic_right
+-/
 
 namespace Monic
 
+#print Polynomial.Monic.natDegree_eq_zero_iff_eq_one /-
 @[simp]
 theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1 :=
   by
@@ -166,12 +221,16 @@ theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1
   rw [← h]
   apply hp
 #align polynomial.monic.nat_degree_eq_zero_iff_eq_one Polynomial.Monic.natDegree_eq_zero_iff_eq_one
+-/
 
+#print Polynomial.Monic.degree_le_zero_iff_eq_one /-
 @[simp]
 theorem degree_le_zero_iff_eq_one (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1 := by
   rw [← hp.nat_degree_eq_zero_iff_eq_one, nat_degree_eq_zero_iff_degree_le_zero]
 #align polynomial.monic.degree_le_zero_iff_eq_one Polynomial.Monic.degree_le_zero_iff_eq_one
+-/
 
+#print Polynomial.Monic.natDegree_mul /-
 theorem natDegree_mul (hp : p.Monic) (hq : q.Monic) :
     (p * q).natDegree = p.natDegree + q.natDegree :=
   by
@@ -179,7 +238,9 @@ theorem natDegree_mul (hp : p.Monic) (hq : q.Monic) :
   apply nat_degree_mul'
   simp [hp.leading_coeff, hq.leading_coeff]
 #align polynomial.monic.nat_degree_mul Polynomial.Monic.natDegree_mul
+-/
 
+#print Polynomial.Monic.degree_mul_comm /-
 theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).degree :=
   by
   by_cases h : q = 0
@@ -188,14 +249,18 @@ theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).deg
   · exact add_comm _ _
   · rwa [hp.leading_coeff, one_mul, leading_coeff_ne_zero]
 #align polynomial.monic.degree_mul_comm Polynomial.Monic.degree_mul_comm
+-/
 
+#print Polynomial.Monic.natDegree_mul' /-
 theorem natDegree_mul' (hp : p.Monic) (hq : q ≠ 0) :
     (p * q).natDegree = p.natDegree + q.natDegree :=
   by
   rw [nat_degree_mul', add_comm]
   simpa [hp.leading_coeff, leading_coeff_ne_zero]
 #align polynomial.monic.nat_degree_mul' Polynomial.Monic.natDegree_mul'
+-/
 
+#print Polynomial.Monic.natDegree_mul_comm /-
 theorem natDegree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q * p).natDegree :=
   by
   by_cases h : q = 0
@@ -203,18 +268,29 @@ theorem natDegree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q *
   rw [hp.nat_degree_mul' h, Polynomial.natDegree_mul', add_comm]
   simpa [hp.leading_coeff, leading_coeff_ne_zero]
 #align polynomial.monic.nat_degree_mul_comm Polynomial.Monic.natDegree_mul_comm
+-/
 
+#print Polynomial.Monic.not_dvd_of_natDegree_lt /-
 theorem not_dvd_of_natDegree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : natDegree q < natDegree p) :
     ¬p ∣ q := by
   rintro ⟨r, rfl⟩
   rw [hp.nat_degree_mul' <| right_ne_zero_of_mul h0] at hl
   exact hl.not_le (Nat.le_add_right _ _)
 #align polynomial.monic.not_dvd_of_nat_degree_lt Polynomial.Monic.not_dvd_of_natDegree_lt
+-/
 
+#print Polynomial.Monic.not_dvd_of_degree_lt /-
 theorem not_dvd_of_degree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : degree q < degree p) : ¬p ∣ q :=
   Monic.not_dvd_of_natDegree_lt hp h0 <| natDegree_lt_natDegree h0 hl
 #align polynomial.monic.not_dvd_of_degree_lt Polynomial.Monic.not_dvd_of_degree_lt
+-/
 
+/- warning: polynomial.monic.next_coeff_mul -> Polynomial.Monic.nextCoeff_mul is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {q : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u1} R _inst_1 p) -> (Polynomial.Monic.{u1} R _inst_1 q) -> (Eq.{succ u1} R (Polynomial.nextCoeff.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) p q)) (HAdd.hAdd.{u1, u1, u1} R R R (instHAdd.{u1} R (Distrib.toHasAdd.{u1} R (NonUnitalNonAssocSemiring.toDistrib.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (Polynomial.nextCoeff.{u1} R _inst_1 p) (Polynomial.nextCoeff.{u1} R _inst_1 q)))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {q : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u1} R _inst_1 p) -> (Polynomial.Monic.{u1} R _inst_1 q) -> (Eq.{succ u1} R (Polynomial.nextCoeff.{u1} R _inst_1 (HMul.hMul.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHMul.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.mul'.{u1} R _inst_1)) p q)) (HAdd.hAdd.{u1, u1, u1} R R R (instHAdd.{u1} R (Distrib.toAdd.{u1} R (NonUnitalNonAssocSemiring.toDistrib.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (Polynomial.nextCoeff.{u1} R _inst_1 p) (Polynomial.nextCoeff.{u1} R _inst_1 q)))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic.next_coeff_mul Polynomial.Monic.nextCoeff_mulₓ'. -/
 theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) :
     nextCoeff (p * q) = nextCoeff p + nextCoeff q :=
   by
@@ -224,6 +300,12 @@ theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) :
     simp [coeff_mul, nat.antidiagonal, hp.leading_coeff, hq.leading_coeff, add_comm]
 #align polynomial.monic.next_coeff_mul Polynomial.Monic.nextCoeff_mul
 
+/- warning: polynomial.monic.eq_one_of_map_eq_one -> Polynomial.Monic.eq_one_of_map_eq_one is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {p : Polynomial.{u1} R _inst_1} {S : Type.{u2}} [_inst_2 : Semiring.{u2} S] [_inst_3 : Nontrivial.{u2} S] (f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)), (Polynomial.Monic.{u1} R _inst_1 p) -> (Eq.{succ u2} (Polynomial.{u2} S _inst_2) (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p) (OfNat.ofNat.{u2} (Polynomial.{u2} S _inst_2) 1 (OfNat.mk.{u2} (Polynomial.{u2} S _inst_2) 1 (One.one.{u2} (Polynomial.{u2} S _inst_2) (Polynomial.hasOne.{u2} S _inst_2))))) -> (Eq.{succ u1} (Polynomial.{u1} R _inst_1) p (OfNat.ofNat.{u1} (Polynomial.{u1} R _inst_1) 1 (OfNat.mk.{u1} (Polynomial.{u1} R _inst_1) 1 (One.one.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.hasOne.{u1} R _inst_1)))))
+but is expected to have type
+  forall {R : Type.{u2}} [_inst_1 : Semiring.{u2} R] {p : Polynomial.{u2} R _inst_1} {S : Type.{u1}} [_inst_2 : Semiring.{u1} S] [_inst_3 : Nontrivial.{u1} S] (f : RingHom.{u2, u1} R S (Semiring.toNonAssocSemiring.{u2} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)), (Polynomial.Monic.{u2} R _inst_1 p) -> (Eq.{succ u1} (Polynomial.{u1} S _inst_2) (Polynomial.map.{u2, u1} R S _inst_1 _inst_2 f p) (OfNat.ofNat.{u1} (Polynomial.{u1} S _inst_2) 1 (One.toOfNat1.{u1} (Polynomial.{u1} S _inst_2) (Polynomial.one.{u1} S _inst_2)))) -> (Eq.{succ u2} (Polynomial.{u2} R _inst_1) p (OfNat.ofNat.{u2} (Polynomial.{u2} R _inst_1) 1 (One.toOfNat1.{u2} (Polynomial.{u2} R _inst_1) (Polynomial.one.{u2} R _inst_1))))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic.eq_one_of_map_eq_one Polynomial.Monic.eq_one_of_map_eq_oneₓ'. -/
 theorem eq_one_of_map_eq_one {S : Type _} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic)
     (map_eq : p.map f = 1) : p = 1 := by
   nontriviality R
@@ -238,6 +320,7 @@ theorem eq_one_of_map_eq_one {S : Type _} [Semiring S] [Nontrivial S] (f : R →
   rw [← hndeg, ← Polynomial.leadingCoeff, hp.leading_coeff, C.map_one]
 #align polynomial.monic.eq_one_of_map_eq_one Polynomial.Monic.eq_one_of_map_eq_one
 
+#print Polynomial.Monic.natDegree_pow /-
 theorem natDegree_pow (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree :=
   by
   induction' n with n hn
@@ -245,14 +328,22 @@ theorem natDegree_pow (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDe
   · rw [pow_succ, hp.nat_degree_mul (hp.pow n), hn]
     ring
 #align polynomial.monic.nat_degree_pow Polynomial.Monic.natDegree_pow
+-/
 
 end Monic
 
+/- warning: polynomial.nat_degree_pow_X_add_C -> Polynomial.natDegree_pow_X_add_c is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Nontrivial.{u1} R] (n : Nat) (r : R), Eq.{1} Nat (Polynomial.natDegree.{u1} R _inst_1 (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (Polynomial.X.{u1} R _inst_1) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) => R -> (Polynomial.{u1} R _inst_1)) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (Polynomial.C.{u1} R _inst_1) r)) n)) n
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Nontrivial.{u1} R] (n : Nat) (r : R), Eq.{1} Nat (Polynomial.natDegree.{u1} R _inst_1 (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R _inst_1) Nat (Polynomial.{u1} R _inst_1) (instHPow.{u1, 0} (Polynomial.{u1} R _inst_1) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R _inst_1) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))))) (HAdd.hAdd.{u1, u1, u1} (Polynomial.{u1} R _inst_1) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) r) (Polynomial.{u1} R _inst_1) (instHAdd.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.add'.{u1} R _inst_1)) (Polynomial.X.{u1} R _inst_1) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R _inst_1) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1))) R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R _inst_1) (Polynomial.semiring.{u1} R _inst_1)))))) (Polynomial.C.{u1} R _inst_1) r)) n)) n
+Case conversion may be inaccurate. Consider using '#align polynomial.nat_degree_pow_X_add_C Polynomial.natDegree_pow_X_add_cₓ'. -/
 @[simp]
-theorem natDegree_pow_x_add_c [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n := by
+theorem natDegree_pow_X_add_c [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n := by
   rw [(monic_X_add_C r).natDegree_pow, nat_degree_X_add_C, mul_one]
-#align polynomial.nat_degree_pow_X_add_C Polynomial.natDegree_pow_x_add_c
+#align polynomial.nat_degree_pow_X_add_C Polynomial.natDegree_pow_X_add_c
 
+#print Polynomial.Monic.eq_one_of_isUnit /-
 theorem Monic.eq_one_of_isUnit (hm : Monic p) (hpu : IsUnit p) : p = 1 :=
   by
   nontriviality R
@@ -261,10 +352,13 @@ theorem Monic.eq_one_of_isUnit (hm : Monic p) (hpu : IsUnit p) : p = 1 :=
   rw [h, nat_degree_one, eq_comm, add_eq_zero_iff] at this
   exact hm.nat_degree_eq_zero_iff_eq_one.mp this.1
 #align polynomial.monic.eq_one_of_is_unit Polynomial.Monic.eq_one_of_isUnit
+-/
 
+#print Polynomial.Monic.isUnit_iff /-
 theorem Monic.isUnit_iff (hm : p.Monic) : IsUnit p ↔ p = 1 :=
   ⟨hm.eq_one_of_isUnit, fun h => h.symm ▸ isUnit_one⟩
 #align polynomial.monic.is_unit_iff Polynomial.Monic.isUnit_iff
+-/
 
 end Semiring
 
@@ -272,6 +366,7 @@ section CommSemiring
 
 variable [CommSemiring R] {p : R[X]}
 
+#print Polynomial.monic_multiset_prod_of_monic /-
 theorem monic_multiset_prod_of_monic (t : Multiset ι) (f : ι → R[X]) (ht : ∀ i ∈ t, Monic (f i)) :
     Monic (t.map f).Prod := by
   revert ht
@@ -280,12 +375,16 @@ theorem monic_multiset_prod_of_monic (t : Multiset ι) (f : ι → R[X]) (ht : 
   rw [Multiset.map_cons, Multiset.prod_cons]
   exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))
 #align polynomial.monic_multiset_prod_of_monic Polynomial.monic_multiset_prod_of_monic
+-/
 
+#print Polynomial.monic_prod_of_monic /-
 theorem monic_prod_of_monic (s : Finset ι) (f : ι → R[X]) (hs : ∀ i ∈ s, Monic (f i)) :
     Monic (∏ i in s, f i) :=
   monic_multiset_prod_of_monic s.1 f hs
 #align polynomial.monic_prod_of_monic Polynomial.monic_prod_of_monic
+-/
 
+#print Polynomial.Monic.nextCoeff_multiset_prod /-
 theorem Monic.nextCoeff_multiset_prod (t : Multiset ι) (f : ι → R[X]) (h : ∀ i ∈ t, Monic (f i)) :
     nextCoeff (t.map f).Prod = (t.map fun i => nextCoeff (f i)).Sum :=
   by
@@ -300,11 +399,14 @@ theorem Monic.nextCoeff_multiset_prod (t : Multiset ι) (f : ι → R[X]) (h : 
     exacts[fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
       monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]
 #align polynomial.monic.next_coeff_multiset_prod Polynomial.Monic.nextCoeff_multiset_prod
+-/
 
+#print Polynomial.Monic.nextCoeff_prod /-
 theorem Monic.nextCoeff_prod (s : Finset ι) (f : ι → R[X]) (h : ∀ i ∈ s, Monic (f i)) :
     nextCoeff (∏ i in s, f i) = ∑ i in s, nextCoeff (f i) :=
   Monic.nextCoeff_multiset_prod s.1 f h
 #align polynomial.monic.next_coeff_prod Polynomial.Monic.nextCoeff_prod
+-/
 
 end CommSemiring
 
@@ -312,6 +414,7 @@ section Semiring
 
 variable [Semiring R]
 
+#print Polynomial.Monic.natDegree_map /-
 @[simp]
 theorem Monic.natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
     (P.map f).natDegree = P.natDegree :=
@@ -320,7 +423,9 @@ theorem Monic.natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Moni
   rw [coeff_map, monic.coeff_nat_degree hmo, RingHom.map_one]
   exact one_ne_zero
 #align polynomial.monic.nat_degree_map Polynomial.Monic.natDegree_map
+-/
 
+#print Polynomial.Monic.degree_map /-
 @[simp]
 theorem Monic.degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
     (P.map f).degree = P.degree := by
@@ -332,6 +437,7 @@ theorem Monic.degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic)
     rw [coeff_map, monic.coeff_nat_degree hmo, RingHom.map_one]
     exact one_ne_zero
 #align polynomial.monic.degree_map Polynomial.Monic.degree_map
+-/
 
 section Injective
 
@@ -341,6 +447,12 @@ variable [Semiring S] {f : R →+* S} (hf : Injective f)
 
 include hf
 
+/- warning: polynomial.degree_map_eq_of_injective -> Polynomial.degree_map_eq_of_injective is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{1} (WithBot.{0} Nat) (Polynomial.degree.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (Polynomial.degree.{u1} R _inst_1 p))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{1} (WithBot.{0} Nat) (Polynomial.degree.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (Polynomial.degree.{u1} R _inst_1 p))
+Case conversion may be inaccurate. Consider using '#align polynomial.degree_map_eq_of_injective Polynomial.degree_map_eq_of_injectiveₓ'. -/
 theorem degree_map_eq_of_injective (p : R[X]) : degree (p.map f) = degree p :=
   if h : p = 0 then by simp [h]
   else
@@ -348,16 +460,34 @@ theorem degree_map_eq_of_injective (p : R[X]) : degree (p.map f) = degree p :=
       (by rw [← f.map_zero] <;> exact mt hf.eq_iff.1 (mt leading_coeff_eq_zero.1 h))
 #align polynomial.degree_map_eq_of_injective Polynomial.degree_map_eq_of_injective
 
+/- warning: polynomial.nat_degree_map_eq_of_injective -> Polynomial.natDegree_map_eq_of_injective is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{1} Nat (Polynomial.natDegree.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (Polynomial.natDegree.{u1} R _inst_1 p))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{1} Nat (Polynomial.natDegree.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (Polynomial.natDegree.{u1} R _inst_1 p))
+Case conversion may be inaccurate. Consider using '#align polynomial.nat_degree_map_eq_of_injective Polynomial.natDegree_map_eq_of_injectiveₓ'. -/
 theorem natDegree_map_eq_of_injective (p : R[X]) : natDegree (p.map f) = natDegree p :=
   natDegree_eq_of_degree_eq (degree_map_eq_of_injective hf p)
 #align polynomial.nat_degree_map_eq_of_injective Polynomial.natDegree_map_eq_of_injective
 
+/- warning: polynomial.leading_coeff_map' -> Polynomial.leadingCoeff_map' is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.leadingCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f (Polynomial.leadingCoeff.{u1} R _inst_1 p)))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.leadingCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f (Polynomial.leadingCoeff.{u1} R _inst_1 p)))
+Case conversion may be inaccurate. Consider using '#align polynomial.leading_coeff_map' Polynomial.leadingCoeff_map'ₓ'. -/
 theorem leadingCoeff_map' (p : R[X]) : leadingCoeff (p.map f) = f (leadingCoeff p) :=
   by
   unfold leading_coeff
   rw [coeff_map, nat_degree_map_eq_of_injective hf p]
 #align polynomial.leading_coeff_map' Polynomial.leadingCoeff_map'
 
+/- warning: polynomial.next_coeff_map -> Polynomial.nextCoeff_map is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.nextCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f (Polynomial.nextCoeff.{u1} R _inst_1 p)))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.nextCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f (Polynomial.nextCoeff.{u1} R _inst_1 p)))
+Case conversion may be inaccurate. Consider using '#align polynomial.next_coeff_map Polynomial.nextCoeff_mapₓ'. -/
 theorem nextCoeff_map (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff :=
   by
   unfold next_coeff
@@ -365,18 +495,36 @@ theorem nextCoeff_map (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff :=
   split_ifs <;> simp
 #align polynomial.next_coeff_map Polynomial.nextCoeff_map
 
+/- warning: polynomial.leading_coeff_of_injective -> Polynomial.leadingCoeff_of_injective is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.leadingCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f (Polynomial.leadingCoeff.{u1} R _inst_1 p)))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall (p : Polynomial.{u1} R _inst_1), Eq.{succ u2} S (Polynomial.leadingCoeff.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f (Polynomial.leadingCoeff.{u1} R _inst_1 p)))
+Case conversion may be inaccurate. Consider using '#align polynomial.leading_coeff_of_injective Polynomial.leadingCoeff_of_injectiveₓ'. -/
 theorem leadingCoeff_of_injective (p : R[X]) : leadingCoeff (p.map f) = f (leadingCoeff p) :=
   by
   delta leading_coeff
   rw [coeff_map f, nat_degree_map_eq_of_injective hf p]
 #align polynomial.leading_coeff_of_injective Polynomial.leadingCoeff_of_injective
 
+/- warning: polynomial.monic_of_injective -> Polynomial.monic_of_injective is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall {p : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) -> (Polynomial.Monic.{u1} R _inst_1 p))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall {p : Polynomial.{u1} R _inst_1}, (Polynomial.Monic.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)) -> (Polynomial.Monic.{u1} R _inst_1 p))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_of_injective Polynomial.monic_of_injectiveₓ'. -/
 theorem monic_of_injective {p : R[X]} (hp : (p.map f).Monic) : p.Monic :=
   by
   apply hf
   rw [← leading_coeff_of_injective hf, hp.leading_coeff, f.map_one]
 #align polynomial.monic_of_injective Polynomial.monic_of_injective
 
+/- warning: function.injective.monic_map_iff -> Function.Injective.monic_map_iff is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (fun (_x : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) f)) -> (forall {p : Polynomial.{u1} R _inst_1}, Iff (Polynomial.Monic.{u1} R _inst_1 p) (Polynomial.Monic.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)))
+but is expected to have type
+  forall {R : Type.{u1}} {S : Type.{u2}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] {f : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)}, (Function.Injective.{succ u1, succ u2} R S (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => S) _x) (MulHomClass.toFunLike.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u2} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S (Semiring.toNonAssocSemiring.{u2} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, u1, u2} (RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2))))) f)) -> (forall {p : Polynomial.{u1} R _inst_1}, Iff (Polynomial.Monic.{u1} R _inst_1 p) (Polynomial.Monic.{u2} S _inst_2 (Polynomial.map.{u1, u2} R S _inst_1 _inst_2 f p)))
+Case conversion may be inaccurate. Consider using '#align function.injective.monic_map_iff Function.Injective.monic_map_iffₓ'. -/
 theorem Function.Injective.monic_map_iff {p : R[X]} : p.Monic ↔ (p.map f).Monic :=
   ⟨Monic.map _, Polynomial.monic_of_injective hf⟩
 #align function.injective.monic_map_iff Function.Injective.monic_map_iff
@@ -389,38 +537,70 @@ section Ring
 
 variable [Ring R] {p : R[X]}
 
-theorem monic_x_sub_c (x : R) : Monic (X - C x) := by
+/- warning: polynomial.monic_X_sub_C -> Polynomial.monic_X_sub_C is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] (x : R), Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) => R -> (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (Polynomial.C.{u1} R (Ring.toSemiring.{u1} R _inst_1)) x))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] (x : R), Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) x) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))))))) (Polynomial.C.{u1} R (Ring.toSemiring.{u1} R _inst_1)) x))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_X_sub_C Polynomial.monic_X_sub_Cₓ'. -/
+theorem monic_X_sub_C (x : R) : Monic (X - C x) := by
   simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)
-#align polynomial.monic_X_sub_C Polynomial.monic_x_sub_c
-
-theorem monic_x_pow_sub {n : ℕ} (H : degree p ≤ n) : Monic (X ^ (n + 1) - p) := by
+#align polynomial.monic_X_sub_C Polynomial.monic_X_sub_C
+
+/- warning: polynomial.monic_X_pow_sub -> Polynomial.monic_X_pow_sub is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] {p : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)} {n : Nat}, (LE.le.{0} (WithBot.{0} Nat) (Preorder.toLE.{0} (WithBot.{0} Nat) (WithBot.preorder.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))))) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) p) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat (WithBot.{0} Nat) (HasLiftT.mk.{1, 1} Nat (WithBot.{0} Nat) (CoeTCₓ.coe.{1, 1} Nat (WithBot.{0} Nat) (WithBot.hasCoeT.{0} Nat))) n)) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Ring.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.ring.{u1} R _inst_1)))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) p))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] {p : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)} {n : Nat}, (LE.le.{0} (WithBot.{0} Nat) (Preorder.toLE.{0} (WithBot.{0} Nat) (WithBot.preorder.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)))) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) p) (Nat.cast.{0} (WithBot.{0} Nat) (Semiring.toNatCast.{0} (WithBot.{0} Nat) (OrderedSemiring.toSemiring.{0} (WithBot.{0} Nat) (OrderedCommSemiring.toOrderedSemiring.{0} (WithBot.{0} Nat) (WithBot.orderedCommSemiring.{0} Nat (fun (a : Nat) (b : Nat) => instDecidableEqNat a b) Nat.canonicallyOrderedCommSemiring Nat.nontrivial)))) n)) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) p))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_X_pow_sub Polynomial.monic_X_pow_subₓ'. -/
+theorem monic_X_pow_sub {n : ℕ} (H : degree p ≤ n) : Monic (X ^ (n + 1) - p) := by
   simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) ≤ n by rwa [← degree_neg p] at H)
-#align polynomial.monic_X_pow_sub Polynomial.monic_x_pow_sub
-
+#align polynomial.monic_X_pow_sub Polynomial.monic_X_pow_sub
+
+/- warning: polynomial.monic_X_pow_sub_C -> Polynomial.monic_X_pow_sub_C is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_2 : Ring.{u1} R] (a : R) {n : Nat}, (Ne.{1} Nat n (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_2) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.sub.{u1} R _inst_2)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Ring.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.ring.{u1} R _inst_2)))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_2)) n) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) (fun (_x : RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) => R -> (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2))) (RingHom.hasCoeToFun.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) (Polynomial.C.{u1} R (Ring.toSemiring.{u1} R _inst_2)) a)))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_2 : Ring.{u1} R] (a : R) {n : Nat}, (Ne.{1} Nat n (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_2) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) a) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.sub.{u1} R _inst_2)) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R _inst_2)) n) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2372 : R) => Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) (NonUnitalNonAssocSemiring.toMul.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2))))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)))) R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2))) (RingHom.instRingHomClassRingHom.{u1, u1} R (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Semiring.toNonAssocSemiring.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_2)) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R _inst_2))))))) (Polynomial.C.{u1} R (Ring.toSemiring.{u1} R _inst_2)) a)))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic_X_pow_sub_C Polynomial.monic_X_pow_sub_Cₓ'. -/
 /-- `X ^ n - a` is monic. -/
-theorem monic_x_pow_sub_c {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).Monic :=
+theorem monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).Monic :=
   by
   obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero h
   convert monic_X_pow_sub _
   exact le_trans degree_C_le Nat.WithBot.coe_nonneg
-#align polynomial.monic_X_pow_sub_C Polynomial.monic_x_pow_sub_c
-
-theorem not_isUnit_x_pow_sub_one (R : Type _) [CommRing R] [Nontrivial R] (n : ℕ) :
+#align polynomial.monic_X_pow_sub_C Polynomial.monic_X_pow_sub_C
+
+/- warning: polynomial.not_is_unit_X_pow_sub_one -> Polynomial.not_isUnit_X_pow_sub_one is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) [_inst_2 : CommRing.{u1} R] [_inst_3 : Nontrivial.{u1} R] (n : Nat), Not (IsUnit.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Ring.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.ring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.sub.{u1} R (CommRing.toRing.{u1} R _inst_2))) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Ring.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.ring.{u1} R (CommRing.toRing.{u1} R _inst_2))))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) n) (OfNat.ofNat.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) 1 (OfNat.mk.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) 1 (One.one.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.hasOne.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))))))))
+but is expected to have type
+  forall (R : Type.{u1}) [_inst_2 : CommRing.{u1} R] [_inst_3 : Nontrivial.{u1} R] (n : Nat), Not (IsUnit.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))))) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.sub.{u1} R (CommRing.toRing.{u1} R _inst_2))) (HPow.hPow.{u1, 0, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) Nat (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (instHPow.{u1, 0} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) Nat (Monoid.Pow.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (MonoidWithZero.toMonoid.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Semiring.toMonoidWithZero.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.semiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))))))) (Polynomial.X.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) n) (OfNat.ofNat.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) 1 (One.toOfNat1.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2))) (Polynomial.one.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_2)))))))
+Case conversion may be inaccurate. Consider using '#align polynomial.not_is_unit_X_pow_sub_one Polynomial.not_isUnit_X_pow_sub_oneₓ'. -/
+theorem not_isUnit_X_pow_sub_one (R : Type _) [CommRing R] [Nontrivial R] (n : ℕ) :
     ¬IsUnit (X ^ n - 1 : R[X]) := by
   intro h
   rcases eq_or_ne n 0 with (rfl | hn)
   · simpa using h
   apply hn
   rw [← @nat_degree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, nat_degree_X_pow_sub_C]
-#align polynomial.not_is_unit_X_pow_sub_one Polynomial.not_isUnit_x_pow_sub_one
+#align polynomial.not_is_unit_X_pow_sub_one Polynomial.not_isUnit_X_pow_sub_one
 
+#print Polynomial.Monic.sub_of_left /-
 theorem Monic.sub_of_left {p q : R[X]} (hp : Monic p) (hpq : degree q < degree p) : Monic (p - q) :=
   by
   rw [sub_eq_add_neg]
   apply hp.add_of_left
   rwa [degree_neg]
 #align polynomial.monic.sub_of_left Polynomial.Monic.sub_of_left
+-/
 
+/- warning: polynomial.monic.sub_of_right -> Polynomial.Monic.sub_of_right is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] {p : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)} {q : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)}, (Eq.{succ u1} R (Polynomial.leadingCoeff.{u1} R (Ring.toSemiring.{u1} R _inst_1) q) (Neg.neg.{u1} R (SubNegMonoid.toHasNeg.{u1} R (AddGroup.toSubNegMonoid.{u1} R (AddGroupWithOne.toAddGroup.{u1} R (NonAssocRing.toAddGroupWithOne.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))))) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (NonAssocRing.toAddGroupWithOne.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))))))))) -> (LT.lt.{0} (WithBot.{0} Nat) (Preorder.toLT.{0} (WithBot.{0} Nat) (WithBot.preorder.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))))) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) p) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) q)) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) p q))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R] {p : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)} {q : Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)}, (Eq.{succ u1} R (Polynomial.leadingCoeff.{u1} R (Ring.toSemiring.{u1} R _inst_1) q) (Neg.neg.{u1} R (Ring.toNeg.{u1} R _inst_1) (OfNat.ofNat.{u1} R 1 (One.toOfNat1.{u1} R (NonAssocRing.toOne.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1)))))) -> (LT.lt.{0} (WithBot.{0} Nat) (Preorder.toLT.{0} (WithBot.{0} Nat) (WithBot.preorder.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)))) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) p) (Polynomial.degree.{u1} R (Ring.toSemiring.{u1} R _inst_1) q)) -> (Polynomial.Monic.{u1} R (Ring.toSemiring.{u1} R _inst_1) (HSub.hSub.{u1, u1, u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (instHSub.{u1} (Polynomial.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Polynomial.sub.{u1} R _inst_1)) p q))
+Case conversion may be inaccurate. Consider using '#align polynomial.monic.sub_of_right Polynomial.Monic.sub_of_rightₓ'. -/
 theorem Monic.sub_of_right {p q : R[X]} (hq : q.leadingCoeff = -1) (hpq : degree p < degree q) :
     Monic (p - q) :=
   by
@@ -437,10 +617,12 @@ section NonzeroSemiring
 
 variable [Semiring R] [Nontrivial R] {p q : R[X]}
 
+#print Polynomial.not_monic_zero /-
 @[simp]
 theorem not_monic_zero : ¬Monic (0 : R[X]) :=
   not_monic_zero_iff.mp zero_ne_one
 #align polynomial.not_monic_zero Polynomial.not_monic_zero
+-/
 
 end NonzeroSemiring
 
@@ -449,6 +631,7 @@ section NotZeroDivisor
 -- TODO: using gh-8537, rephrase lemmas that involve commutation around `*` using the op-ring
 variable [Semiring R] {p : R[X]}
 
+#print Polynomial.Monic.mul_left_ne_zero /-
 theorem Monic.mul_left_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p ≠ 0 :=
   by
   by_cases h : p = 1
@@ -459,7 +642,9 @@ theorem Monic.mul_left_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p
   refine' (lt_trans _ h).ne'
   simp
 #align polynomial.monic.mul_left_ne_zero Polynomial.Monic.mul_left_ne_zero
+-/
 
+#print Polynomial.Monic.mul_right_ne_zero /-
 theorem Monic.mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q ≠ 0 :=
   by
   by_cases h : p = 1
@@ -471,7 +656,9 @@ theorem Monic.mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q
   refine' (lt_trans _ h).ne'
   simp
 #align polynomial.monic.mul_right_ne_zero Polynomial.Monic.mul_right_ne_zero
+-/
 
+#print Polynomial.Monic.mul_natDegree_lt_iff /-
 theorem Monic.mul_natDegree_lt_iff (h : Monic p) {q : R[X]} :
     (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0 :=
   by
@@ -480,15 +667,21 @@ theorem Monic.mul_natDegree_lt_iff (h : Monic p) {q : R[X]} :
     exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
   · simp [h.nat_degree_mul', hq]
 #align polynomial.monic.mul_nat_degree_lt_iff Polynomial.Monic.mul_natDegree_lt_iff
+-/
 
+#print Polynomial.Monic.mul_right_eq_zero_iff /-
 theorem Monic.mul_right_eq_zero_iff (h : Monic p) {q : R[X]} : p * q = 0 ↔ q = 0 := by
   by_cases hq : q = 0 <;> simp [h.mul_right_ne_zero, hq]
 #align polynomial.monic.mul_right_eq_zero_iff Polynomial.Monic.mul_right_eq_zero_iff
+-/
 
+#print Polynomial.Monic.mul_left_eq_zero_iff /-
 theorem Monic.mul_left_eq_zero_iff (h : Monic p) {q : R[X]} : q * p = 0 ↔ q = 0 := by
   by_cases hq : q = 0 <;> simp [h.mul_left_ne_zero, hq]
 #align polynomial.monic.mul_left_eq_zero_iff Polynomial.Monic.mul_left_eq_zero_iff
+-/
 
+#print Polynomial.Monic.isRegular /-
 theorem Monic.isRegular {R : Type _} [Ring R] {p : R[X]} (hp : Monic p) : IsRegular p :=
   by
   constructor
@@ -498,7 +691,14 @@ theorem Monic.isRegular {R : Type _} [Ring R] {p : R[X]} (hp : Monic p) : IsRegu
     simp only at h
     rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
 #align polynomial.monic.is_regular Polynomial.Monic.isRegular
+-/
 
+/- warning: polynomial.degree_smul_of_smul_regular -> Polynomial.degree_smul_of_smul_regular is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {S : Type.{u2}} [_inst_2 : Monoid.{u2} S] [_inst_3 : DistribMulAction.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))] {k : S} (p : Polynomial.{u1} R _inst_1), (IsSMulRegular.{u2, u1} S R (SMulZeroClass.toHasSmul.{u2, u1} S R (AddZeroClass.toHasZero.{u1} R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))) (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3))) k) -> (Eq.{1} (WithBot.{0} Nat) (Polynomial.degree.{u1} R _inst_1 (SMul.smul.{u2, u1} S (Polynomial.{u1} R _inst_1) (SMulZeroClass.toHasSmul.{u2, u1} S (Polynomial.{u1} R _inst_1) (Polynomial.zero.{u1} R _inst_1) (Polynomial.smulZeroClass.{u1, u2} R _inst_1 S (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3)))) k p)) (Polynomial.degree.{u1} R _inst_1 p))
+but is expected to have type
+  forall {R : Type.{u2}} [_inst_1 : Semiring.{u2} R] {S : Type.{u1}} [_inst_2 : Monoid.{u1} S] [_inst_3 : DistribMulAction.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))] {k : S} (p : Polynomial.{u2} R _inst_1), (IsSMulRegular.{u1, u2} S R (SMulZeroClass.toSMul.{u1, u2} S R (MonoidWithZero.toZero.{u2} R (Semiring.toMonoidWithZero.{u2} R _inst_1)) (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))) k) -> (Eq.{1} (WithBot.{0} Nat) (Polynomial.degree.{u2} R _inst_1 (HSMul.hSMul.{u1, u2, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.{u2} R _inst_1) (instHSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (SMulZeroClass.toSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.zero.{u2} R _inst_1) (Polynomial.smulZeroClass.{u2, u1} R _inst_1 S (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))))) k p)) (Polynomial.degree.{u2} R _inst_1 p))
+Case conversion may be inaccurate. Consider using '#align polynomial.degree_smul_of_smul_regular Polynomial.degree_smul_of_smul_regularₓ'. -/
 theorem degree_smul_of_smul_regular {S : Type _} [Monoid S] [DistribMulAction S R] {k : S}
     (p : R[X]) (h : IsSMulRegular R k) : (k • p).degree = p.degree :=
   by
@@ -514,6 +714,12 @@ theorem degree_smul_of_smul_regular {S : Type _} [Monoid S] [DistribMulAction S
     simpa using hm m le_rfl
 #align polynomial.degree_smul_of_smul_regular Polynomial.degree_smul_of_smul_regular
 
+/- warning: polynomial.nat_degree_smul_of_smul_regular -> Polynomial.natDegree_smul_of_smul_regular is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {S : Type.{u2}} [_inst_2 : Monoid.{u2} S] [_inst_3 : DistribMulAction.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))] {k : S} (p : Polynomial.{u1} R _inst_1), (IsSMulRegular.{u2, u1} S R (SMulZeroClass.toHasSmul.{u2, u1} S R (AddZeroClass.toHasZero.{u1} R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))) (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3))) k) -> (Eq.{1} Nat (Polynomial.natDegree.{u1} R _inst_1 (SMul.smul.{u2, u1} S (Polynomial.{u1} R _inst_1) (SMulZeroClass.toHasSmul.{u2, u1} S (Polynomial.{u1} R _inst_1) (Polynomial.zero.{u1} R _inst_1) (Polynomial.smulZeroClass.{u1, u2} R _inst_1 S (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3)))) k p)) (Polynomial.natDegree.{u1} R _inst_1 p))
+but is expected to have type
+  forall {R : Type.{u2}} [_inst_1 : Semiring.{u2} R] {S : Type.{u1}} [_inst_2 : Monoid.{u1} S] [_inst_3 : DistribMulAction.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))] {k : S} (p : Polynomial.{u2} R _inst_1), (IsSMulRegular.{u1, u2} S R (SMulZeroClass.toSMul.{u1, u2} S R (MonoidWithZero.toZero.{u2} R (Semiring.toMonoidWithZero.{u2} R _inst_1)) (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))) k) -> (Eq.{1} Nat (Polynomial.natDegree.{u2} R _inst_1 (HSMul.hSMul.{u1, u2, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.{u2} R _inst_1) (instHSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (SMulZeroClass.toSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.zero.{u2} R _inst_1) (Polynomial.smulZeroClass.{u2, u1} R _inst_1 S (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))))) k p)) (Polynomial.natDegree.{u2} R _inst_1 p))
+Case conversion may be inaccurate. Consider using '#align polynomial.nat_degree_smul_of_smul_regular Polynomial.natDegree_smul_of_smul_regularₓ'. -/
 theorem natDegree_smul_of_smul_regular {S : Type _} [Monoid S] [DistribMulAction S R] {k : S}
     (p : R[X]) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree :=
   by
@@ -526,11 +732,18 @@ theorem natDegree_smul_of_smul_regular {S : Type _} [Monoid S] [DistribMulAction
   exact h.polynomial hp
 #align polynomial.nat_degree_smul_of_smul_regular Polynomial.natDegree_smul_of_smul_regular
 
+/- warning: polynomial.leading_coeff_smul_of_smul_regular -> Polynomial.leadingCoeff_smul_of_smul_regular is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] {S : Type.{u2}} [_inst_2 : Monoid.{u2} S] [_inst_3 : DistribMulAction.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))] {k : S} (p : Polynomial.{u1} R _inst_1), (IsSMulRegular.{u2, u1} S R (SMulZeroClass.toHasSmul.{u2, u1} S R (AddZeroClass.toHasZero.{u1} R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))) (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3))) k) -> (Eq.{succ u1} R (Polynomial.leadingCoeff.{u1} R _inst_1 (SMul.smul.{u2, u1} S (Polynomial.{u1} R _inst_1) (SMulZeroClass.toHasSmul.{u2, u1} S (Polynomial.{u1} R _inst_1) (Polynomial.zero.{u1} R _inst_1) (Polynomial.smulZeroClass.{u1, u2} R _inst_1 S (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3)))) k p)) (SMul.smul.{u2, u1} S R (SMulZeroClass.toHasSmul.{u2, u1} S R (AddZeroClass.toHasZero.{u1} R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))))) (DistribSMul.toSmulZeroClass.{u2, u1} S R (AddMonoid.toAddZeroClass.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))))) (DistribMulAction.toDistribSMul.{u2, u1} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) _inst_3))) k (Polynomial.leadingCoeff.{u1} R _inst_1 p)))
+but is expected to have type
+  forall {R : Type.{u2}} [_inst_1 : Semiring.{u2} R] {S : Type.{u1}} [_inst_2 : Monoid.{u1} S] [_inst_3 : DistribMulAction.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))] {k : S} (p : Polynomial.{u2} R _inst_1), (IsSMulRegular.{u1, u2} S R (SMulZeroClass.toSMul.{u1, u2} S R (MonoidWithZero.toZero.{u2} R (Semiring.toMonoidWithZero.{u2} R _inst_1)) (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))) k) -> (Eq.{succ u2} R (Polynomial.leadingCoeff.{u2} R _inst_1 (HSMul.hSMul.{u1, u2, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.{u2} R _inst_1) (instHSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (SMulZeroClass.toSMul.{u1, u2} S (Polynomial.{u2} R _inst_1) (Polynomial.zero.{u2} R _inst_1) (Polynomial.smulZeroClass.{u2, u1} R _inst_1 S (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3))))) k p)) (HSMul.hSMul.{u1, u2, u2} S R R (instHSMul.{u1, u2} S R (SMulZeroClass.toSMul.{u1, u2} S R (MonoidWithZero.toZero.{u2} R (Semiring.toMonoidWithZero.{u2} R _inst_1)) (DistribSMul.toSMulZeroClass.{u1, u2} S R (AddMonoid.toAddZeroClass.{u2} R (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1))))) (DistribMulAction.toDistribSMul.{u1, u2} S R _inst_2 (AddMonoidWithOne.toAddMonoid.{u2} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u2} R (NonAssocSemiring.toAddCommMonoidWithOne.{u2} R (Semiring.toNonAssocSemiring.{u2} R _inst_1)))) _inst_3)))) k (Polynomial.leadingCoeff.{u2} R _inst_1 p)))
+Case conversion may be inaccurate. Consider using '#align polynomial.leading_coeff_smul_of_smul_regular Polynomial.leadingCoeff_smul_of_smul_regularₓ'. -/
 theorem leadingCoeff_smul_of_smul_regular {S : Type _} [Monoid S] [DistribMulAction S R] {k : S}
     (p : R[X]) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff := by
   rw [leading_coeff, leading_coeff, coeff_smul, nat_degree_smul_of_smul_regular p h]
 #align polynomial.leading_coeff_smul_of_smul_regular Polynomial.leadingCoeff_smul_of_smul_regular
 
+#print Polynomial.monic_of_isUnit_leadingCoeff_inv_smul /-
 theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) : Monic (h.Unit⁻¹ • p) :=
   by
   rw [monic.def, leading_coeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
@@ -538,7 +751,9 @@ theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) : Moni
   simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
   simp [Units.ext_iff, IsUnit.unit_spec]
 #align polynomial.monic_of_is_unit_leading_coeff_inv_smul Polynomial.monic_of_isUnit_leadingCoeff_inv_smul
+-/
 
+#print Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff /-
 theorem isUnit_leadingCoeff_mul_right_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
     p * q = 0 ↔ q = 0 := by
   constructor
@@ -555,7 +770,9 @@ theorem isUnit_leadingCoeff_mul_right_eq_zero_iff (h : IsUnit p.leadingCoeff) {q
   · rintro rfl
     simp
 #align polynomial.is_unit_leading_coeff_mul_right_eq_zero_iff Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff
+-/
 
+#print Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff /-
 theorem isUnit_leadingCoeff_mul_left_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
     q * p = 0 ↔ q = 0 := by
   constructor
@@ -568,6 +785,7 @@ theorem isUnit_leadingCoeff_mul_left_eq_zero_iff (h : IsUnit p.leadingCoeff) {q
   · rintro rfl
     rw [zero_mul]
 #align polynomial.is_unit_leading_coeff_mul_left_eq_zero_iff Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff
+-/
 
 end NotZeroDivisor
 
diff --git a/Mathbin/Data/Polynomial/RingDivision.lean b/Mathbin/Data/Polynomial/RingDivision.lean
index c3ddcff7a9..df026fbf81 100644
--- a/Mathbin/Data/Polynomial/RingDivision.lean
+++ b/Mathbin/Data/Polynomial/RingDivision.lean
@@ -1052,7 +1052,7 @@ theorem pairwise_coprime_x_sub_c {K} [Field K] {I : Type v} {s : I → K} (H : F
 #align polynomial.pairwise_coprime_X_sub_C Polynomial.pairwise_coprime_x_sub_c
 
 theorem monic_prod_multiset_x_sub_c : Monic (p.roots.map fun a => X - C a).Prod :=
-  monic_multiset_prod_of_monic _ _ fun a _ => monic_x_sub_c a
+  monic_multiset_prod_of_monic _ _ fun a _ => monic_X_sub_C a
 #align polynomial.monic_prod_multiset_X_sub_C Polynomial.monic_prod_multiset_x_sub_c
 
 theorem prod_multiset_root_eq_finset_root :
diff --git a/Mathbin/FieldTheory/Minpoly/Field.lean b/Mathbin/FieldTheory/Minpoly/Field.lean
index 9c8c1113a9..33c56e9dcc 100644
--- a/Mathbin/FieldTheory/Minpoly/Field.lean
+++ b/Mathbin/FieldTheory/Minpoly/Field.lean
@@ -271,7 +271,7 @@ theorem root {x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y)
     algebraMap A B y = x :=
   by
   have key : minpoly A x = X - C y :=
-    eq_of_monic_of_associated (monic hx) (monic_x_sub_c y)
+    eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
       (associated_of_dvd_dvd
         ((irreducible_x_sub_c y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
         (dvd_iff_isRoot.2 h))
diff --git a/Mathbin/RingTheory/IntegralClosure.lean b/Mathbin/RingTheory/IntegralClosure.lean
index deb0799512..0a31b69fab 100644
--- a/Mathbin/RingTheory/IntegralClosure.lean
+++ b/Mathbin/RingTheory/IntegralClosure.lean
@@ -79,7 +79,7 @@ protected def Algebra.IsIntegral : Prop :=
 variable {R A}
 
 theorem RingHom.is_integral_map {x : R} : f.IsIntegralElem (f x) :=
-  ⟨X - C x, monic_x_sub_c _, by simp⟩
+  ⟨X - C x, monic_X_sub_C _, by simp⟩
 #align ring_hom.is_integral_map RingHom.is_integral_map
 
 theorem isIntegral_algebraMap {x : R} : IsIntegral R (algebraMap R A x) :=
diff --git a/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean
index c6746403bf..cab80978f9 100644
--- a/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean
+++ b/Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean
@@ -105,7 +105,7 @@ theorem cyclotomic'_two (R : Type _) [CommRing R] [IsDomain R] (p : ℕ) [CharP
 /-- `cyclotomic' n R` is monic. -/
 theorem cyclotomic'.monic (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] :
     (cyclotomic' n R).Monic :=
-  monic_prod_of_monic _ _ fun z hz => monic_x_sub_c _
+  monic_prod_of_monic _ _ fun z hz => monic_X_sub_C _
 #align polynomial.cyclotomic'.monic Polynomial.cyclotomic'.monic
 
 /-- `cyclotomic' n R` is different from `0`. -/
diff --git a/lake-manifest.json b/lake-manifest.json
index fedd2855b5..9e1e265694 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "da1463c8620c9fcc3d9a770aa52f0c5a66390c2e",
+    "rev": "9f7b25530726cbd5bfd6d1a93b5bde7b836a0426",
     "name": "lean3port",
-    "inputRev?": "da1463c8620c9fcc3d9a770aa52f0c5a66390c2e"}},
+    "inputRev?": "9f7b25530726cbd5bfd6d1a93b5bde7b836a0426"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "69108c782429c57637807f32d923e34c195ec823",
+    "rev": "0ee6690d078a47e95313b4a53c5dcfea78d8269e",
     "name": "mathlib",
-    "inputRev?": "69108c782429c57637807f32d923e34c195ec823"}},
+    "inputRev?": "0ee6690d078a47e95313b4a53c5dcfea78d8269e"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index ee60e6016f..84430c1f50 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-09-12"
+def tag : String := "nightly-2023-03-09-14"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"da1463c8620c9fcc3d9a770aa52f0c5a66390c2e"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9f7b25530726cbd5bfd6d1a93b5bde7b836a0426"
 
 @[default_target]
 lean_lib Mathbin where