chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas (#31817)

Author: kckennylau

Mathlib/Algebra/Polynomial/CoeffMem.lean

@@ -111,9 +111,9 @@ lemma coeff_divByMonic_mem_pow_natDegree_mul (p q : S[X])
 variable [DecidableEq ι] {i j : ι}
 
 open Function Ideal in
-lemma idealSpan_range_update_divByMonic (hij : i ≠ j) (v : ι → R[X]) (hi : (v i).Monic) :
+lemma idealSpan_range_update_divByMonic (hij : i ≠ j) (v : ι → R[X]) :
     span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v) := by
-  rw [modByMonic_eq_sub_mul_div _ hi, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
+  rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
     Submodule.span_range_update_sub_smul hij]
 
 end Polynomial

Mathlib/Algebra/Polynomial/Div.lean

@@ -220,32 +220,33 @@ theorem X_dvd_sub_C : X ∣ p - C (p.coeff 0) := by
   simp [X_dvd_iff, coeff_C]
 
 theorem modByMonic_eq_sub_mul_div :
-    ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), p %ₘ q = p - q * (p /ₘ q)
-  | p, q, hq =>
+    ∀ p q : R[X], p %ₘ q = p - q * (p /ₘ q)
+  | p, q =>
     letI := Classical.decEq R
-    if h : degree q ≤ degree p ∧ p ≠ 0 then by
-      have _wf := div_wf_lemma h hq
-      have ih := modByMonic_eq_sub_mul_div
-        (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
-      unfold modByMonic divByMonic divModByMonicAux
-      dsimp
-      rw [dif_pos hq, if_pos h]
-      rw [modByMonic, dif_pos hq] at ih
-      refine ih.trans ?_
-      unfold divByMonic
-      rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub]
+    if hq : q.Monic then
+      if h : degree q ≤ degree p ∧ p ≠ 0 then by
+        have _wf := div_wf_lemma h hq
+        have ih := modByMonic_eq_sub_mul_div
+          (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) q
+        unfold modByMonic divByMonic divModByMonicAux
+        rw [dif_pos hq, dif_pos h]
+        rw [modByMonic, dif_pos hq] at ih
+        refine ih.trans ?_
+        rw [divByMonic, dif_pos hq, dif_pos hq, dif_pos h, mul_add, sub_add_eq_sub_sub]
+      else by
+        unfold modByMonic divByMonic divModByMonicAux
+        dsimp
+        rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
     else by
-      unfold modByMonic divByMonic divModByMonicAux
-      dsimp
-      rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
+      rw [modByMonic_eq_of_not_monic _ hq, divByMonic_eq_of_not_monic _ hq, mul_zero, sub_zero]
   termination_by p => p
 
-theorem modByMonic_add_div (p : R[X]) {q : R[X]} (hq : Monic q) : p %ₘ q + q * (p /ₘ q) = p :=
-  eq_sub_iff_add_eq.1 (modByMonic_eq_sub_mul_div p hq)
+theorem modByMonic_add_div (p q : R[X]) : p %ₘ q + q * (p /ₘ q) = p :=
+  eq_sub_iff_add_eq.1 (modByMonic_eq_sub_mul_div p q)
 
 theorem divByMonic_eq_zero_iff [Nontrivial R] (hq : Monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
   ⟨fun h => by
-    have := modByMonic_add_div p hq
+    have := modByMonic_add_div p q
     rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this,
   fun h => by
     classical
@@ -268,7 +269,7 @@ theorem degree_add_divByMonic (hq : Monic q) (h : degree q ≤ degree p) :
   calc
     degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
     _ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
-    _ = _ := congr_arg _ (modByMonic_add_div _ hq)
+    _ = _ := congr_arg _ (modByMonic_add_div _ _)
 
 theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
   letI := Classical.decEq R
@@ -285,20 +286,24 @@ theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
         simp [dif_pos hq, h, degree_zero, bot_le]
     else (divByMonic_eq_of_not_monic p hq).symm ▸ bot_le
 
-theorem degree_divByMonic_lt (p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0)
+theorem degree_divByMonic_lt (p q : R[X]) (hp0 : p ≠ 0)
     (h0q : 0 < degree q) : degree (p /ₘ q) < degree p :=
-  if hpq : degree p < degree q then by
-    haveI := Nontrivial.of_polynomial_ne hp0
-    rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
-    exact WithBot.bot_lt_coe _
+  letI := Classical.decEq R
+  if hq : q.Monic then
+    if hpq : degree p < degree q then by
+      haveI := Nontrivial.of_polynomial_ne hp0
+      rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
+      exact WithBot.bot_lt_coe _
+    else by
+      haveI := Nontrivial.of_polynomial_ne hp0
+      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
+        Nat.cast_lt.2
+          (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
+            by simpa [degree_eq_natDegree hq.ne_zero] using h0q))
   else by
-    haveI := Nontrivial.of_polynomial_ne hp0
-    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
-      Nat.cast_lt.2
-        (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
-          by simpa [degree_eq_natDegree hq.ne_zero] using h0q))
+    rwa [divByMonic_eq_of_not_monic _ hq, degree_zero, bot_lt_iff_ne_bot, degree_ne_bot]
 
 theorem natDegree_divByMonic (f : R[X]) {g : R[X]} (hg : g.Monic) :
     natDegree (f /ₘ g) = natDegree f - natDegree g := by
@@ -325,7 +330,7 @@ theorem div_modByMonic_unique {f g} (q r : R[X]) (hg : Monic g)
   have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
     eq_of_sub_eq_zero
       (by
-        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
+        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
         simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
   have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
   have h₄ : degree (r - f %ₘ g) < degree g :=
@@ -349,7 +354,7 @@ theorem map_mod_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
   haveI : Nontrivial R := f.domain_nontrivial
   have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
     div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
-      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
+      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
         calc
           _ ≤ degree (p %ₘ q) := degree_map_le
           _ < degree q := degree_modByMonic_lt _ hq
@@ -368,11 +373,11 @@ theorem map_modByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
   (map_mod_divByMonic f hq).2
 
 theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p :=
-  ⟨fun h => by rw [← modByMonic_add_div p hq, h, zero_add]; exact dvd_mul_right _ _, fun h => by
+  ⟨fun h => by rw [← modByMonic_add_div p q, h, zero_add]; exact dvd_mul_right _ _, fun h => by
     nontriviality R
     obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
     by_contra hpq0
-    have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
+    have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
     have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
     have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
       hpq0 <|
@@ -405,7 +410,7 @@ theorem modByMonic_one (p : R[X]) : p %ₘ 1 = 0 :=
 
 @[simp]
 theorem divByMonic_one (p : R[X]) : p /ₘ 1 = p := by
-  conv_rhs => rw [← modByMonic_add_div p monic_one]; simp
+  conv_rhs => rw [← modByMonic_add_div p 1]; simp
 
 theorem sum_modByMonic_coeff (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ n) :
     (∑ i : Fin n, monomial i ((p %ₘ q).coeff i)) = p %ₘ q := by
@@ -426,7 +431,7 @@ lemma coeff_divByMonic_X_sub_C_rec (p : R[X]) (a : R) (n : ℕ) :
   nontriviality R
   have := monic_X_sub_C a
   set q := p /ₘ (X - C a)
-  rw [← p.modByMonic_add_div this]
+  rw [← p.modByMonic_add_div (X - C a)]
   have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
     |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
   simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]
@@ -536,8 +541,7 @@ theorem pow_mul_divByMonic_rootMultiplicity_eq (p : R[X]) (a : R) :
     (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p := by
   have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
   conv_rhs =>
-      rw [← modByMonic_add_div p this,
-        (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
+    rw [← modByMonic_add_div p, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
   simp
 
 theorem exists_eq_pow_rootMultiplicity_mul_and_not_dvd (p : R[X]) (hp : p ≠ 0) (a : R) :
@@ -558,7 +562,7 @@ variable [CommRing R] {p p₁ p₂ q : R[X]}
 theorem modByMonic_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a) := by
   nontriviality R
   have h : (p %ₘ (X - C a)).eval a = p.eval a := by
-    rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
+    rw [modByMonic_eq_sub_mul_div, eval_sub, eval_mul, eval_sub, eval_X,
       eval_C, sub_self, zero_mul, sub_zero]
   have : degree (p %ₘ (X - C a)) < 1 :=
     degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
@@ -574,9 +578,7 @@ theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ Is
   .trans
     ⟨fun h => by rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
     fun h => by
-      conv_rhs =>
-        rw [← modByMonic_add_div p (monic_X_sub_C a)]
-        rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
+      conv_rhs => rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
     IsRoot.def.symm
 
 theorem dvd_iff_isRoot : X - C a ∣ p ↔ IsRoot p a :=
@@ -592,9 +594,9 @@ theorem X_sub_C_dvd_sub_C_eval : X - C a ∣ p - C (p.eval a) := by
 theorem modByMonic_X (p : R[X]) : p %ₘ X = C (p.eval 0) := by
   rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]
 
-theorem eval₂_modByMonic_eq_self_of_root [CommRing S] {f : R →+* S} {p q : R[X]} (hq : q.Monic)
+theorem eval₂_modByMonic_eq_self_of_root [CommRing S] {f : R →+* S} {p q : R[X]}
     {x : S} (hx : q.eval₂ f x = 0) : (p %ₘ q).eval₂ f x = p.eval₂ f x := by
-  rw [modByMonic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
+  rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
 
 theorem sub_dvd_eval_sub (a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b := by
   suffices X - C b ∣ p - C (p.eval b) by
@@ -646,7 +648,7 @@ lemma modByMonic_eq_of_dvd_sub (hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %
   nontriviality R
   obtain ⟨f, sub_eq⟩ := h
   refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2
-  rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div _ hq, add_comm]
+  rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]
 
 lemma add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q := by
   by_cases hq : q.Monic
@@ -655,8 +657,8 @@ lemma add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p
     · exact
       (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
           ⟨by
-            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
-              add_comm (q * _), modByMonic_add_div _ hq],
+            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
+              add_comm (q * _), modByMonic_add_div],
             (degree_add_le _ _).trans_lt
               (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2
   · simp_rw [modByMonic_eq_of_not_monic _ hq]
@@ -745,7 +747,7 @@ lemma leadingCoeff_divByMonic_of_monic (hmonic : q.Monic)
   have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
     simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
       Nat.WithBot.one_le_iff_zero_lt] using hdegree
-  nth_rw 2 [← modByMonic_add_div p hmonic]
+  nth_rw 2 [← modByMonic_add_div p q]
   rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
   rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
   exact (degree_modByMonic_lt p hmonic).trans_le hdegree

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -313,7 +313,7 @@ private theorem quotient_mul_add_remainder_eq_aux (p q : R[X]) : q * div p q + m
   · simp only [h, zero_mul, mod, modByMonic_zero, zero_add]
   · conv =>
       rhs
-      rw [← modByMonic_add_div p (monic_mul_leadingCoeff_inv h)]
+      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]
     rw [div, mod, add_comm, mul_assoc]
 
 private theorem remainder_lt_aux (p : R[X]) (hq : q ≠ 0) : degree (mod p q) < degree q := by
@@ -396,7 +396,7 @@ theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p := by
 theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p := by
   have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
   rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
-  exact degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
+  exact degree_divByMonic_lt _ (q * C q.leadingCoeff⁻¹) hp
     (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)
 
 theorem isUnit_map [Field k] (f : R →+* k) : IsUnit (p.map f) ↔ IsUnit p := by
@@ -625,7 +625,6 @@ theorem degree_pos_of_irreducible (hp : Irreducible p) : 0 < p.degree :=
 theorem X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type*} [Ring K] (f : K[X]) (a : K) :
     (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a) := by
   rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
-  exact monic_X_sub_C a
 
 theorem divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative
     {K : Type*} [CommRing K] (f : K[X]) (a : K) :

Mathlib/Algebra/Polynomial/PartialFractions.lean

@@ -74,8 +74,8 @@ theorem div_eq_quo_add_rem_div_add_rem_div (f : R[X]) {g₁ g₂ : R[X]} (hg₁
   have hg₂' : (↑g₂ : K) ≠ 0 := by
     norm_cast
     exact hg₂.ne_zero
-  have hfc := modByMonic_add_div (f * c) hg₂
-  have hfd := modByMonic_add_div (f * d) hg₁
+  have hfc := modByMonic_add_div (f * c) g₂
+  have hfd := modByMonic_add_div (f * d) g₁
   field_simp
   norm_cast
   linear_combination -1 * f * hcd + -1 * g₁ * hfc + -1 * g₂ * hfd

Mathlib/Algebra/Polynomial/RingDivision.lean

@@ -56,7 +56,7 @@ theorem smul_modByMonic (c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q) :
     · simp only [eq_iff_true_of_subsingleton]
     · exact
       (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
-          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq],
+          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div],
             (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2
   · simp_rw [modByMonic_eq_of_not_monic _ hq]
 
@@ -75,11 +75,10 @@ section
 
 variable [Ring S]
 
-theorem aeval_modByMonic_eq_self_of_root [Algebra R S] {p q : R[X]} (hq : q.Monic) {x : S}
+theorem aeval_modByMonic_eq_self_of_root [Algebra R S] {p q : R[X]} {x : S}
     (hx : aeval x q = 0) : aeval x (p %ₘ q) = aeval x p := by
-    --`eval₂_modByMonic_eq_self_of_root` doesn't work here as it needs commutativity
-  rw [modByMonic_eq_sub_mul_div p hq, map_sub, map_mul, hx, zero_mul,
-    sub_zero]
+  --`eval₂_modByMonic_eq_self_of_root` doesn't work here as it needs commutativity
+  rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]
 
 end
 
@@ -262,7 +261,7 @@ theorem exists_multiset_roots [DecidableEq R] :
       have hd0 : p /ₘ (X - C x) ≠ 0 := fun h => by
         rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp; exact hp rfl
       have wf : degree (p /ₘ (X - C x)) < degree p :=
-        degree_divByMonic_lt _ (monic_X_sub_C x) hp ((degree_X_sub_C x).symm ▸ by decide)
+        degree_divByMonic_lt _ _ hp ((degree_X_sub_C x).symm ▸ by decide)
       let ⟨t, htd, htr⟩ := @exists_multiset_roots _ (p /ₘ (X - C x)) hd0
       have hdeg : degree (X - C x) ≤ degree p := by
         rw [degree_X_sub_C, degree_eq_natDegree hp]

Mathlib/FieldTheory/Minpoly/Basic.lean

@@ -143,7 +143,7 @@ theorem unique' {p : A[X]} (hm : p.Monic) (hp : Polynomial.aeval x p = 0)
   have hx : IsIntegral A x := ⟨p, hm, hp⟩
   obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
   swap
-  · exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
+  · exact (h <| (aeval_modByMonic_eq_self_of_root hp).trans <| aeval A x).elim
   obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 h
   rw [hr]
   have hlead := congr_arg leadingCoeff hr

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -76,7 +76,7 @@ theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p := by
   rw [← modByMonic_eq_zero_iff_dvd (monic hx)]
   by_contra hnz
   apply degree_le_of_ne_zero A x hnz
-    ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp) |>.not_gt
+    ((aeval_modByMonic_eq_self_of_root (aeval _ _)).trans hp) |>.not_gt
   exact degree_modByMonic_lt _ (monic hx)
 
 variable {A x} in

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -76,12 +76,11 @@ theorem isIntegrallyClosed_dvd {s : S} (hs : IsIntegral R s) {p : R[X]}
   let _ : Algebra K L := FractionRing.liftAlgebra R L
   have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) := by
     rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
-    · refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
-      · rw [← map_aeval_eq_aeval_map, hp, map_zero]
-        rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-      apply dvd_mul_of_dvd_left
-      rw [isIntegrallyClosed_eq_field_fractions K L hs]
-    exact Monic.map _ (minpoly.monic hs)
+    refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
+    · rw [← map_aeval_eq_aeval_map, hp, map_zero]
+      rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
+    apply dvd_mul_of_dvd_left
+    rw [isIntegrallyClosed_eq_field_fractions K L hs]
   rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
     map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
   rw [← modByMonic_eq_zero_iff_dvd (minpoly.monic hs)]

Mathlib/LinearAlgebra/Charpoly/Basic.lean

@@ -103,7 +103,7 @@ theorem minpoly_dvd_charpoly {K : Type u} {M : Type v} [Field K] [AddCommGroup M
 /-- Any endomorphism polynomial `p` is equivalent under evaluation to `p %ₘ f.charpoly`; that is,
 `p` is equivalent to a polynomial with degree less than the dimension of the module. -/
 theorem aeval_eq_aeval_mod_charpoly (p : R[X]) : aeval f p = aeval f (p %ₘ f.charpoly) :=
-  (aeval_modByMonic_eq_self_of_root f.charpoly_monic f.aeval_self_charpoly).symm
+  (aeval_modByMonic_eq_self_of_root f.aeval_self_charpoly).symm
 
 /-- Any endomorphism power can be computed as the sum of endomorphism powers less than the
 dimension of the module. -/

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -247,7 +247,7 @@ namespace Matrix
 is equivalent to a polynomial with degree less than the dimension of the matrix. -/
 theorem aeval_eq_aeval_mod_charpoly (M : Matrix n n R) (p : R[X]) :
     aeval M p = aeval M (p %ₘ M.charpoly) :=
-  (aeval_modByMonic_eq_self_of_root M.charpoly_monic M.aeval_self_charpoly).symm
+  (aeval_modByMonic_eq_self_of_root M.aeval_self_charpoly).symm
 
 /-- Any matrix power can be computed as the sum of matrix powers less than `Fintype.card n`.
 
@@ -359,7 +359,7 @@ lemma isNilpotent_charpoly_sub_pow_of_isNilpotent (hM : IsNilpotent M) :
   nontriviality R
   let p : R[X] := M.charpolyRev
   have hp : p - 1 = X * (p /ₘ X) := by
-    conv_lhs => rw [← modByMonic_add_div p monic_X]
+    conv_lhs => rw [← modByMonic_add_div p X]
     simp [p, modByMonic_X]
   have : IsNilpotent (p /ₘ X) :=
     (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2