feat: WithTop.charZero (#6992)

Also `WithBot.charZero`

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Algebra.Order.ZeroLEOne
+import Mathlib.Algebra.CharZero.Defs
 
 #align_import algebra.order.monoid.with_top from "leanprover-community/mathlib"@"0111834459f5d7400215223ea95ae38a1265a907"
 
@@ -351,6 +352,10 @@ instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (WithTop α)
       rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one]
   }
 
+instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α) :=
+  { cast_injective := Function.Injective.comp (f := Nat.cast (R := α))
+      (fun _ _ => WithTop.coe_eq_coe.1) Nat.cast_injective}
+
 instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α) :=
   { WithTop.addMonoidWithOne, WithTop.addCommMonoid with }
 
@@ -490,6 +495,9 @@ instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (WithBot α) :=
 instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (WithBot α) :=
   WithTop.addMonoidWithOne
 
+instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α) :=
+  WithTop.charZero
+
 instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithBot α) :=
   WithTop.addCommMonoidWithOne
 

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -65,7 +65,7 @@ theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).
   · rw [degree_eq_natDegree h]
     suffices (l.map natDegree).maximum = ((l.map natDegree).foldr max 0 : ℕ) by
       rw [this]
-      simpa [this, Nat.cast_withBot] using natDegree_list_sum_le l
+      simpa using natDegree_list_sum_le l
     rw [← List.foldr_max_of_ne_nil]
     · congr
     contrapose! h

Mathlib/Data/Polynomial/Degree/CardPowDegree.lean

@@ -100,8 +100,7 @@ theorem cardPowDegree_isEuclidean : IsEuclidean (cardPowDegree : AbsoluteValue F
       · simp only [hp, hq, degree_zero, Ne.def, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
           not_false_iff]
       · simp only [hp, hq, degree_zero, not_lt_bot, (pow_pos _).not_lt]
-      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_withBot, Nat.cast_withBot,
-          WithBot.coe_lt_coe, pow_lt_pow_iff]
+      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff]
         exact_mod_cast @Fintype.one_lt_card Fq _ _ }
 #align polynomial.card_pow_degree_is_euclidean Polynomial.cardPowDegree_isEuclidean
 

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -238,7 +238,6 @@ theorem natDegree_lt_natDegree {p q : R[X]} (hp : p ≠ 0) (hpq : p.degree < q.d
     p.natDegree < q.natDegree := by
   by_cases hq : q = 0
   · exact (not_lt_bot <| hq ▸ hpq).elim
-  -- Porting note: `Nat.cast_withBot` is required.
   rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
 #align polynomial.nat_degree_lt_nat_degree Polynomial.natDegree_lt_natDegree
 

Mathlib/Data/Polynomial/Degree/Lemmas.lean

@@ -69,8 +69,7 @@ theorem degree_pos_of_root {p : R[X]} (hp : p ≠ 0) (h : IsRoot p a) : 0 < degr
 #align polynomial.degree_pos_of_root Polynomial.degree_pos_of_root
 
 theorem natDegree_le_iff_coeff_eq_zero : p.natDegree ≤ n ↔ ∀ N : ℕ, n < N → p.coeff N = 0 := by
-  simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_withBot,
-    WithBot.coe_lt_coe]
+  simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]
 #align polynomial.nat_degree_le_iff_coeff_eq_zero Polynomial.natDegree_le_iff_coeff_eq_zero
 
 theorem natDegree_add_le_iff_left {n : ℕ} (p q : R[X]) (qn : q.natDegree ≤ n) :
@@ -287,7 +286,7 @@ theorem degree_pos_of_eval₂_root {p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z
 theorem coe_lt_degree {p : R[X]} {n : ℕ} : (n : WithBot ℕ) < degree p ↔ n < natDegree p := by
   by_cases h : p = 0
   · simp [h]
-  simp [degree_eq_natDegree h, Nat.cast_withBot, WithBot.coe_lt_coe]
+  simp [degree_eq_natDegree h, Nat.cast_lt]
 #align polynomial.coe_lt_degree Polynomial.coe_lt_degree
 
 end Degree

Mathlib/Data/Polynomial/Derivative.lean

@@ -370,7 +370,6 @@ theorem degree_derivative_eq [NoZeroSMulDivisors ℕ R] (p : R[X]) (hp : 0 < nat
   · rw [derivative_apply]
     apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
     intro n hn
-    simp only [Nat.cast_withBot]
     apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
     apply le_natDegree_of_mem_supp _ hn
   · refine' le_sup _

Mathlib/Data/Polynomial/Div.lean

@@ -75,9 +75,8 @@ theorem multiplicity_finite_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < deg
     have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
       simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def,
           hr0]
-    have hnp : 0 < natDegree p := by
-      rw [← WithBot.coe_lt_coe, ← Nat.cast_withBot, ← Nat.cast_withBot,
-        ← degree_eq_natDegree hp0]; exact hp
+    have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
+      rw [← degree_eq_natDegree hp0]; exact hp
     have := congr_arg natDegree hr
     rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
     exact
@@ -98,9 +97,8 @@ theorem div_wf_lemma (h : degree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
   have hp : leadingCoeff p ≠ 0 := mt leadingCoeff_eq_zero.1 h.2
   have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne h.2
   have hlt : natDegree q ≤ natDegree p :=
-    WithBot.coe_le_coe.1
-      (by rw [← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree h.2,
-        ← degree_eq_natDegree hq0]; exact h.1)
+    Nat.cast_le.1
+      (by rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1)
   degree_sub_lt
     (by
       rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
@@ -270,7 +268,7 @@ theorem degree_add_divByMonic (hq : Monic q) (h : degree q ≤ degree p) :
       degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
       _ ≤ _ := by
         rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
-            Nat.cast_add, Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_le_coe]
+            Nat.cast_add, Nat.cast_le]
         exact Nat.le_add_right _ _
   calc
     degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
@@ -304,9 +302,9 @@ theorem degree_divByMonic_lt (p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0
     rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
       degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
     exact
-      WithBot.coe_lt_coe.2
-        (Nat.lt_add_of_pos_left (WithBot.coe_lt_coe.1 <|
-          by simpa [Nat.cast_withBot, degree_eq_natDegree hq.ne_zero] using h0q))
+      Nat.cast_lt.2
+        (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
+          by simpa [degree_eq_natDegree hq.ne_zero] using h0q))
 #align polynomial.degree_div_by_monic_lt Polynomial.degree_divByMonic_lt
 
 theorem natDegree_divByMonic {R : Type u} [CommRing R] (f : R[X]) {g : R[X]} (hg : g.Monic) :
@@ -325,8 +323,7 @@ theorem natDegree_divByMonic {R : Type u} [CommRing R] (f : R[X]) {g : R[X]} (hg
     apply hfg
     rw [hf, zero_divByMonic]
   rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
-    Nat.cast_withBot, Nat.cast_withBot, Nat.cast_withBot,
-    ← WithBot.coe_add, WithBot.coe_eq_coe] at this
+    ← Nat.cast_add, Nat.cast_inj] at this
   rw [← this, add_tsub_cancel_left]
 #align polynomial.nat_degree_div_by_monic Polynomial.natDegree_divByMonic
 

Mathlib/Data/Polynomial/Monic.lean

@@ -496,8 +496,7 @@ theorem natDegree_smul_of_smul_regular {S : Type*} [Monoid S] [DistribMulAction
     (p : R[X]) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree := by
   by_cases hp : p = 0
   · simp [hp]
-  rw [← WithBot.coe_eq_coe, ← Nat.cast_withBot, ←Nat.cast_withBot,
-      ← degree_eq_natDegree hp, ← degree_eq_natDegree,
+  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree,
     degree_smul_of_smul_regular p h]
   contrapose! hp
   rw [← smul_zero k] at hp

Mathlib/Data/Polynomial/Reverse.lean

@@ -273,7 +273,7 @@ theorem reverse_eq_zero : f.reverse = 0 ↔ f = 0 := by simp [reverse]
 theorem reverse_natDegree_le (f : R[X]) : f.reverse.natDegree ≤ f.natDegree := by
   rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]
   intro n hn
-  rw [Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe] at hn
+  rw [Nat.cast_lt] at hn
   rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
     coeff_eq_zero_of_natDegree_lt hn]
 #align polynomial.reverse_nat_degree_le Polynomial.reverse_natDegree_le

Mathlib/Data/Polynomial/RingDivision.lean

@@ -133,9 +133,8 @@ instance : NoZeroDivisors R[X] where
     rw [← leadingCoeff_zero, ← leadingCoeff_mul, h]
 
 theorem natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegree + q.natDegree := by
-  rw [← WithBot.coe_eq_coe, ← Nat.cast_withBot, ←degree_eq_natDegree (mul_ne_zero hp hq),
-    WithBot.coe_add, ← Nat.cast_withBot, ←degree_eq_natDegree hp, ← Nat.cast_withBot,
-    ← degree_eq_natDegree hq, degree_mul]
+  rw [← Nat.cast_inj (R := WithBot ℕ), ←degree_eq_natDegree (mul_ne_zero hp hq),
+    Nat.cast_add,  ←degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]
 #align polynomial.nat_degree_mul Polynomial.natDegree_mul
 
 theorem trailingDegree_mul : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree := by
@@ -525,8 +524,8 @@ theorem exists_multiset_roots [DecidableEq R] :
 termination_by _ p _ => natDegree p
 decreasing_by {
   simp_wf
-  apply WithBot.coe_lt_coe.mp
-  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0, ←Nat.cast_withBot] at wf;
+  apply (Nat.cast_lt (α := WithBot ℕ)).mp
+  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf;
   assumption}
 #align polynomial.exists_multiset_roots Polynomial.exists_multiset_roots
 
@@ -821,8 +820,7 @@ theorem card_nthRoots (n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n :=
             rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
             exact degree_C_le))
   else by
-    rw [← WithBot.coe_le_coe]
-    simp only [← Nat.cast_withBot]
+    rw [← Nat.cast_le (α := WithBot ℕ)]
     rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
     exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))
 #align polynomial.card_nth_roots Polynomial.card_nthRoots

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -74,8 +74,7 @@ theorem charpoly_sub_diagonal_degree_lt :
   apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
   rw [mem_degreeLT]
   apply lt_of_le_of_lt degree_le_natDegree _
-  rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
-  rw [WithBot.coe_lt_coe]
+  rw [Nat.cast_lt]
   apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
   apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
   rw [card_eq_sum_ones]; rw [sum_filter]; apply sum_le_sum
@@ -88,8 +87,7 @@ theorem charpoly_coeff_eq_prod_coeff_of_le {k : ℕ} (h : Fintype.card n - 1 ≤
   apply eq_of_sub_eq_zero; rw [← coeff_sub]
   apply Polynomial.coeff_eq_zero_of_degree_lt
   apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_
-  rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
-  rw [WithBot.coe_le_coe]; apply h
+  rw [Nat.cast_le]; apply h
 #align matrix.charpoly_coeff_eq_prod_coeff_of_le Matrix.charpoly_coeff_eq_prod_coeff_of_le
 
 theorem det_of_card_zero (h : Fintype.card n = 0) (M : Matrix n n R) : M.det = 1 := by
@@ -119,8 +117,7 @@ theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
   exact h1
   rw [h1]
   apply lt_trans (charpoly_sub_diagonal_degree_lt M)
-  rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
-  rw [WithBot.coe_lt_coe]
+  rw [Nat.cast_lt]
   rw [← Nat.pred_eq_sub_one]
   apply Nat.pred_lt
   apply h
@@ -146,8 +143,7 @@ theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic := by
   rw [← neg_sub]
   rw [degree_neg]
   apply lt_trans (charpoly_sub_diagonal_degree_lt M)
-  rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
-  rw [WithBot.coe_lt_coe]
+  rw [Nat.cast_lt]
   rw [← Nat.pred_eq_sub_one]
   apply Nat.pred_lt
   apply h

Mathlib/RingTheory/AdjoinRoot.lean

@@ -552,8 +552,7 @@ theorem minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff
       rfl
     · simp only [RingHom.comp_apply, mk_X, lift_root]
   rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
-    Nat.cast_withBot, Nat.cast_withBot, -- porting note: added
-    WithBot.coe_le_coe, natDegree_mul hf, natDegree_C, add_zero]
+    Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]
   apply natDegree_le_of_dvd
   · have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
     exact mk_eq_zero.1 this

Mathlib/RingTheory/EisensteinCriterion.lean

@@ -52,10 +52,10 @@ set_option linter.uppercaseLean3 false in
 theorem le_natDegree_of_map_eq_mul_X_pow {n : ℕ} {P : Ideal R} (hP : P.IsPrime) {q : R[X]}
     {c : Polynomial (R ⧸ P)} (hq : map (mk P) q = c * X ^ n) (hc0 : c.degree = 0) :
     n ≤ q.natDegree :=
-  WithBot.coe_le_coe.1
+  Nat.cast_le.1
     (calc
       ↑n = degree (q.map (mk P)) := by
-        rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one, Nat.cast_withBot]
+        rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one]
       _ ≤ degree q := (degree_map_le _ _)
       _ ≤ natDegree q := degree_le_natDegree
       )

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -155,8 +155,7 @@ def degreeLTEquiv (R) [Semiring R] (n : ℕ) : degreeLT R n ≃ₗ[R] Fin n →
     by_cases hp0 : p = 0
     · subst hp0
       simp only [coeff_zero, LinearMap.map_zero, Finset.sum_const_zero]
-    rw [mem_degreeLT, degree_eq_natDegree hp0,
-      Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe] at hp
+    rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp
     conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
   right_inv f := by
     ext i
@@ -235,7 +234,7 @@ theorem Monic.geom_sum {P : R[X]} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : 
   refine' lt_of_le_of_lt (degree_sum_le _ _) _
   rw [Finset.sup_lt_iff]
   · simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
-    simp only [Nat.cast_withBot, WithBot.coe_lt_coe, hP.natDegree_pow]
+    simp only [Nat.cast_lt, hP.natDegree_pow]
     intro k
     exact nsmul_lt_nsmul hdeg
   · rw [bot_lt_iff_ne_bot, Ne.def, degree_eq_bot]
@@ -573,7 +572,7 @@ theorem mem_leadingCoeffNth (n : ℕ) (x) :
     refine' ⟨p * X ^ (n - natDegree p), ⟨_, I.mul_mem_right _ hpI⟩, _⟩
     · apply le_trans (degree_mul_le _ _) _
       apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
-      rw [Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add, this, Nat.cast_withBot]
+      rw [← Nat.cast_add, this]
     · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]
 #align ideal.mem_leading_coeff_nth Ideal.mem_leadingCoeffNth
 
@@ -592,8 +591,7 @@ theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤
   refine' ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, _, leadingCoeff_mul_X_pow⟩
   refine' le_trans (degree_mul_le _ _) _
   refine' le_trans (add_le_add hpdeg (degree_X_pow_le _)) _
-  rw [Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add, add_tsub_cancel_of_le H,
-    Nat.cast_withBot]
+  rw [← Nat.cast_add, add_tsub_cancel_of_le H]
 #align ideal.leading_coeff_nth_mono Ideal.leadingCoeffNth_mono
 
 theorem mem_leadingCoeff (x) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x := by
@@ -871,8 +869,7 @@ instance (priority := 100) {R : Type*} [CommRing R] [IsDomain R] [WfDvdMonoid R]
         rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]; rfl
       · apply Prod.Lex.left
         rw [Polynomial.degree_eq_natDegree cne0] at *
-        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0,
-          Nat.cast_withBot, Nat.cast_withBot,← WithBot.coe_add, WithBot.coe_lt_coe]
+        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
         exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero fun h => hdeg (h.symm ▸ WithBot.coe_zero))
 
 end Polynomial
@@ -936,8 +933,7 @@ protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNo
           have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
             rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
             rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
-            rw [Nat.cast_withBot, Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add,
-              add_tsub_cancel_of_le, hn]
+            rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
             · refine' le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
             rw [Polynomial.leadingCoeff_X_pow, mul_one]
             exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
@@ -951,8 +947,7 @@ protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNo
             · rw [hpq]
               exact Ideal.zero_mem _
             refine' ih _ _ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
-            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_withBot, Nat.cast_withBot,
-              WithBot.coe_lt_coe, hn] at this
+            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
           exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩⟩⟩
 #align polynomial.is_noetherian_ring Polynomial.isNoetherianRing
 

Mathlib/RingTheory/Polynomial/Content.lean

@@ -365,23 +365,22 @@ theorem content_mul {p q : R[X]} : (p * q).content = p.content * q.content := by
     induction' n with n ih
     · intro p q hpq
       dsimp at hpq
-      rw [Nat.cast_withBot, WithBot.coe_zero,
+      rw [Nat.cast_zero,
         Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
       rcases hpq with (rfl | rfl) <;> simp
     intro p q hpq
     by_cases p0 : p = 0
     · simp [p0]
     by_cases q0 : q = 0
     · simp [q0]
-    rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_withBot,
-      Nat.cast_withBot, WithBot.coe_lt_coe, Nat.lt_succ_iff_lt_or_eq, ←
-      WithBot.coe_lt_coe, ←Nat.cast_withBot, ← degree_eq_natDegree (mul_ne_zero p0 q0),
-      natDegree_mul p0 q0] at hpq
+    rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt,
+      Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ),
+      ← degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq
     rcases hpq with (hlt | heq)
     · apply ih _ _ hlt
-    rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← WithBot.coe_eq_coe,
-      WithBot.coe_add, ← Nat.cast_withBot, ←degree_eq_natDegree p.primPart_ne_zero,
-      ← Nat.cast_withBot, ← degree_eq_natDegree q.primPart_ne_zero] at heq
+    rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← Nat.cast_inj (R := WithBot ℕ),
+      Nat.cast_add, ←degree_eq_natDegree p.primPart_ne_zero,
+      ← degree_eq_natDegree q.primPart_ne_zero] at heq
     rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
     suffices h : (q.primPart * p.primPart).content = 1
     · rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul,
@@ -393,11 +392,11 @@ theorem content_mul {p q : R[X]} : (p * q).content = p.content * q.content := by
       content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart, one_mul,
       mul_comm q.primPart, content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
       content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart]
-    · rw [Nat.cast_withBot, ← heq, degree_mul, WithBot.add_lt_add_iff_right]
+    · rw [← heq, degree_mul, WithBot.add_lt_add_iff_right]
       · apply degree_erase_lt p.primPart_ne_zero
       · rw [Ne.def, degree_eq_bot]
         apply q.primPart_ne_zero
-    · rw [mul_comm, Nat.cast_withBot, ← heq, degree_mul, WithBot.add_lt_add_iff_left]
+    · rw [mul_comm, ← heq, degree_mul, WithBot.add_lt_add_iff_left]
       · apply degree_erase_lt q.primPart_ne_zero
       · rw [Ne.def, degree_eq_bot]
         apply p.primPart_ne_zero