bump 4.32

CompPoly/Bivariate/ToPoly.lean

@@ -313,8 +313,6 @@ lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     ofPoly (0 : R[X][Y]) = 0 := by
       unfold CBivariate.ofPoly
       simp +decide [ Polynomial.support ]
-      erw [Finsupp.support_zero]
-      exact Finset.sum_empty
 
 /-- Ring hom from computable bivariates to Mathlib bivariates. -/
 noncomputable def toPolyRingHom

CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean

@@ -660,6 +660,7 @@ lemma initial_tiled_coeffs_correctness (h_ℓ : ℓ ≤ r) (a : Fin (2 ^ ℓ) 
   simp only [Nat.getLowBits_eq_mod_two_pow]
 
 omit [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 in
+set_option maxHeartbeats 10000000 in
 lemma NTTStage_correctness (i : Fin (ℓ))
     (input_buffer : Fin (2 ^ (ℓ + R_rate)) → L) (original_coeffs : Fin (2 ^ ℓ) → L) :
     additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate (evaluation_buffer := input_buffer)
@@ -762,7 +763,7 @@ lemma NTTStage_correctness (i : Fin (ℓ))
       conv_lhs =>
         enter [1]
         simp only [h_j_div_2_pow_left]
-      congr
+      congr 1
       simp only [even_coeffs_poly, cur_coeffs]
       have h_res := evenRefinement_eq_novel_poly_of_0_leading_suffix 𝔽q β h_ℓ_add_R_rate
         ⟨i, by omega⟩ ⟨Nat.getLowBits i.val j.val, by
@@ -848,7 +849,7 @@ lemma NTTStage_correctness (i : Fin (ℓ))
             simp only [h_k, ↓reduceIte]
         rw [h_get_lsb_eq]
         apply Nat.sum_of_and_eq_zero_is_or h_lsb_and_two_pow_eq_zero
-      congr
+      simp only [h_v_eq]
     rw [h_even_split, h_odd_split]
     rw [h_P_i_split_even_odd]
     have h_x0_eq_cur_evaluation_point : x0 = cur_evaluation_point := by

CompPoly/Fields/Binary/BF128Ghash/Basic.lean

@@ -184,15 +184,19 @@ def ofGF2 : ZMod 2 →+* BF128Ghash := algebraMap (ZMod 2) BF128Ghash
 /-- The generator of the field (root of the GHASH polynomial). -/
 def root : BF128Ghash := AdjoinRoot.root ghashPoly
 
+set_option maxRecDepth 100000 in
 /-- The root satisfies the GHASH polynomial equation:
     root^128 + root^7 + root^2 + root + 1 = 0 -/
 theorem root_satisfies_poly : root^128 + root^7 + root^2 + root + 1 = 0 := by
-  unfold root ghashPoly
-  have h := AdjoinRoot.eval₂_root ghashPoly
-  unfold ghashPoly at h
-  simp only [eval₂_add, eval₂_X, eval₂_one] at h
-  erw [eval₂_pow, eval₂_X, eval₂_pow, eval₂_X, eval₂_pow, eval₂_X] at h
-  exact h
+  calc
+    _ = (AdjoinRoot.mk ghashPoly X)^128 + (AdjoinRoot.mk ghashPoly X)^7 +
+        (AdjoinRoot.mk ghashPoly X)^2 + AdjoinRoot.mk ghashPoly X + 1 := by
+      simp only [root, AdjoinRoot.mk_X]
+    _ = AdjoinRoot.mk ghashPoly (X^128 + X^7 + X^2 + X + 1) := by
+      rw [map_add, map_add, map_add, map_add, map_pow, map_pow, map_pow, map_one]
+    _ = 0 := by
+      change AdjoinRoot.mk ghashPoly ghashPoly = 0
+      exact AdjoinRoot.mk_self
 
 /-- BF128Ghash is a finite type. -/
 instance : Fintype BF128Ghash := by
@@ -204,6 +208,7 @@ instance : Fintype BF128Ghash := by
     exact Finite.of_equiv (Fin pb.dim →₀ ZMod 2) (pb.basis.repr.toEquiv.symm)
   exact Fintype.ofFinite BF128Ghash
 
+set_option maxRecDepth 100000 in
 /-- The cardinality of BF128Ghash is 2^128. -/
 theorem BF128Ghash_card : Fintype.card BF128Ghash = 2^128 := by
   -- Use the fact that AdjoinRoot of an irreducible polynomial of degree d

CompPoly/Fields/Binary/BF128Ghash/Impl.lean

@@ -420,10 +420,10 @@ instance : AddCommGroup ConcreteBF128Ghash where
   nsmul := fun n x => if n % 2 = 0 then 0 else x
   zsmul := fun n x => if n % 2 = 0 then 0 else x
   nsmul_zero := fun x => by
-    simp only [Nat.zero_mod, ↓reduceIte, ofNat_eq_ofNat]
+    rfl
   nsmul_succ := nsmul_succ
   zsmul_zero' := fun x => by
-    simp only [EuclideanDomain.zero_mod, ↓reduceIte, ofNat_eq_ofNat]
+    rfl
   zsmul_succ' := zsmul_succ
   zsmul_neg' := zsmul_neg
 
@@ -605,14 +605,20 @@ lemma intCast_negSucc (n : ℕ) : intCast (Int.negSucc n) = -(↑(n + 1) : Concr
       simp only [natCast_eq, natCast, h_mod]; rfl
     rw [h_nat]; rfl
 
-instance : Ring ConcreteBF128Ghash where
+instance instSemigroupConcreteBF128Ghash : Semigroup ConcreteBF128Ghash where
+  mul_assoc := mul_assoc
+
+instance instRingConcreteBF128Ghash : Ring ConcreteBF128Ghash where
   mul_assoc := mul_assoc
   one_mul := one_mul
   mul_one := mul_one
   left_distrib := left_distrib
   right_distrib := right_distrib
   zero_mul := zero_mul
   mul_zero := mul_zero
+  npow := npowRecAuto
+  npow_zero := by intro x; rfl
+  npow_succ := by intro n x; rfl
   natCast := natCast
   natCast_zero := natCast_zero
   natCast_succ := natCast_succ
@@ -825,8 +831,10 @@ instance instHDivConcreteBF128Ghash : HDiv (ConcreteBF128Ghash) (ConcreteBF128Gh
 
 lemma div_eq_mul_inv (a b : ConcreteBF128Ghash) : a / b = a * b⁻¹ := by rfl
 
-instance : DivisionRing ConcreteBF128Ghash where
-  toRing := inferInstance
+set_option maxRecDepth 100000 in
+set_option maxHeartbeats 10000000 in
+instance instDivisionRingConcreteBF128Ghash : DivisionRing ConcreteBF128Ghash where
+  toRing := instRingConcreteBF128Ghash
   inv := Inv.inv
   exists_pair_ne := exists_pair_ne
   mul_inv_cancel := mul_inv_cancel
@@ -841,7 +849,7 @@ lemma mul_comm (a b : ConcreteBF128Ghash) : a * b = b * a := by
   exact _root_.mul_comm (toQuot a) (toQuot b)
 
 instance instFieldConcreteBF128Ghash : Field ConcreteBF128Ghash where
-  toDivisionRing := inferInstance
+  toDivisionRing := instDivisionRingConcreteBF128Ghash
   mul_comm := mul_comm
 
 end DivisionRing_Field_Instances

CompPoly/Fields/Binary/Tower/Concrete/Basis.lean

@@ -235,7 +235,7 @@ theorem minPoly_of_powerBasisSucc_generator (k : ℕ) :
         let r := q.coeff 0
         have hc : c = q.leadingCoeff := by
           rw [Polynomial.leadingCoeff]
-          exact congrArg q.toFinsupp.2 (id (Eq.symm hqNatDeg))
+          exact congrArg q.toFinsupp.coeff (id (Eq.symm hqNatDeg))
         have hc_ne_zero : c ≠ 0 := by
           rw [hc]
           by_contra h_c_eq_zero

CompPoly/Multivariate/MvPolyEquiv/Core.lean

@@ -31,7 +31,7 @@ def fromCMvPolynomial  (p : CMvPolynomial n R) : MvPolynomial (Fin n) R :=
   let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp
   let toFun (f : Fin n →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0
   let mem_support_fun {a : Fin n →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind
-  Finsupp.mk support.toFinset toFun (by simp [mem_support_fun])
+  AddMonoidAlgebra.ofCoeff <| Finsupp.mk support.toFinset toFun (by simp [mem_support_fun])
 
 noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n R :=
   let ⟨s, f, _⟩ := p
@@ -114,7 +114,8 @@ lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _
 
 omit [BEq R] [LawfulBEq R] in
 lemma coeff_eq {m} (a : CMvPolynomial n R) :
-    MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := rfl
+    MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := by
+  rfl
 
 @[aesop simp]
 lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial n R} :

CompPoly/Multivariate/MvPolyEquiv/Instances.lean

@@ -191,7 +191,8 @@ lemma foldl_eq_sum {β : Type*} [AddCommMonoid β]
     {t : CMvPolynomial n R}
     {f : CMvMonomial n → R → β} :
     ExtTreeMap.foldl (fun x m c => (f m c) + x) 0 t.1 =
-      Finsupp.sum (fromCMvPolynomial t) (f ∘ CMvMonomial.ofFinsupp) := by
+      Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial t))
+        (f ∘ CMvMonomial.ofFinsupp) := by
   unfold Finsupp.sum Finset.sum
   simp only [Function.comp_apply, add_comm]
   rw [ExtTreeMap.foldl_eq_foldl_toList]
@@ -221,8 +222,9 @@ lemma coeff_sum [AddCommMonoid α]
 lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial
     {f : (Fin n →₀ ℕ) → R → Lawful n R }
     {a : CMvPolynomial n R} :
-    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) f) =
-      Finsupp.sum (fromCMvPolynomial a) (fun m c ↦ fromCMvPolynomial (f m c)) := by
+    fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) f) =
+      Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a))
+        (fun m c ↦ fromCMvPolynomial (f m c)) := by
   unfold Finsupp.sum; ext
   simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
 
@@ -231,51 +233,57 @@ lemma map_mul (a b : CMvPolynomial n R) :
     fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b := by
   dsimp only [HMul.hMul, Mul.mul, Lawful.mul, Unlawful.mul]
   simp only [CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful]
-  unfold MonoidAlgebra.mul'
+  unfold AddMonoidAlgebra.mul'
   rw [foldl_eq_sum]; simp_rw [foldl_eq_sum]
   let F₀ (p q) : CMvMonomial n → R → Lawful n R :=
     fun p_1 q_1 ↦ Lawful.fromUnlawful {(p + p_1 , q * q_1)}
   set F₁ : (Fin n →₀ ℕ) → R → Lawful n R :=
-    (fun p q ↦ Finsupp.sum (fromCMvPolynomial b) (F₀ p q ∘ CMvMonomial.ofFinsupp))
+    (fun p q ↦ Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial b))
+      (F₀ p q ∘ CMvMonomial.ofFinsupp))
       ∘ CMvMonomial.ofFinsupp with eqF₁
   let F₂ a₁ b₁ :
-    Multiplicative (Fin n →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (Fin n →₀ ℕ)) :=
-    fun a₂ b₂ ↦ MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
-  set F₃ : Multiplicative (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R :=
-    fun a₁ b₁ ↦ Finsupp.sum (fromCMvPolynomial b) (F₂ a₁ b₁) with eqF₃
-  have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (Fin n →₀ ℕ)} {c₁ : R} :
+    (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R :=
+    fun a₂ b₂ ↦ AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
+  set F₃ : (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R :=
+    fun a₁ b₁ ↦ Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial b)) (F₂ a₁ b₁) with eqF₃
+  have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Fin n →₀ ℕ} {c₁ : R} :
       fromCMvPolynomial (F₁ m₁ c₁) = F₃ m₁ c₁ := by
     dsimp only [Function.comp_apply, F₁, F₀, F₃, F₂]
     rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
     simp only [Function.comp_apply]
     congr
-    ext (m₂ : Multiplicative _) c₂ m
+    ext (m₂ : Fin n →₀ ℕ) c₂ m
     rw [coeff_eq]
     unfold coeff Lawful.fromUnlawful
-    erw [Unlawful.filter_get, ←CMvMonomial.map_mul, ExtTreeMap.singleton_eq_insert]
+    erw [Unlawful.filter_get,
+      ←CMvMonomial.map_mul (m₁ := Multiplicative.ofAdd m₁) (m₂ := Multiplicative.ofAdd m₂),
+      ExtTreeMap.singleton_eq_insert]
     erw [ExtTreeMap.getElem?_insert]
-    by_cases m_in : m = m₁ * m₂
-    · rw [←m_in]
+    by_cases m_in : m = m₁ + m₂
+    · subst m
+      have hmono : CMvMonomial.ofFinsupp (Multiplicative.ofAdd m₁ * Multiplicative.ofAdd m₂) =
+          CMvMonomial.ofFinsupp (m₁ + m₂) := rfl
+      rw [hmono]
       simp only [compare_self]
-      unfold MvPolynomial.coeff MonoidAlgebra.single
-      simp only [m_in, ite_true, Option.getD_some]
+      unfold MvPolynomial.coeff AddMonoidAlgebra.single
+      simp only [ite_true, Option.getD_some]
       erw [Finsupp.single_eq_same]
     · simp only
         [ Std.compare_eq_iff_eq,
           ExtTreeMap.not_mem_empty,
           not_false_eq_true,
           getElem?_neg
         ]
-      unfold MvPolynomial.coeff MonoidAlgebra.single
+      unfold MvPolynomial.coeff AddMonoidAlgebra.single
       erw [Finsupp.single_eq_of_ne (by symm; grind)]
       split
       next h contra =>
         exfalso; apply m_in; symm
         apply CMvMonomial.injective_ofFinsupp contra
       next h => simp_all only [Option.getD_none]
   -- Lean 4.29 may beta-reduce F₃; fold it back then rewrite
-  change fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) F₁) =
-    Finsupp.sum (fromCMvPolynomial a) F₃
+  change fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) F₁) =
+    Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) F₃
   rw [show F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) from by
     ext x; rw [fromCMvPolynomial_F₁_eq_F₃]]
   rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
@@ -309,7 +317,10 @@ instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where
   natCast_zero := rfl
   natCast_succ := by intro n; simp
   npow_zero := by intro x; simp [npowRecAuto, npowRec]
-  npow_succ := by intro n x; simp [npowRecAuto, npowRec]
+  npow_succ := by
+    intro n x
+    change x ^ (n + 1) = x ^ n * x
+    exact pow_succ x n
   mul_comm a b := by
     apply fromCMvPolynomial_injective
     simp [mul_comm]

CompPoly/Multivariate/Operations.lean

@@ -413,8 +413,8 @@ lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {k : ℕ}
 lemma fromCMvPolynomial_finsupp_sum {n k : ℕ} [CommSemiring R] [BEq R] [LawfulBEq R]
     (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R)
     (a : CMvPolynomial n R) :
-    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
-    Finsupp.sum (fromCMvPolynomial a)
+    fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) g) =
+    Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a))
       (fun μ c => fromCMvPolynomial (g μ c)) := by
   unfold Finsupp.sum; ext
   simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]

CompPoly/Multivariate/Rename.lean

@@ -108,8 +108,8 @@ lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
 lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
     (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R)
     (a : CMvPolynomial n R) :
-    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
-    Finsupp.sum (fromCMvPolynomial a)
+    fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) g) =
+    Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a))
       (fun μ c => fromCMvPolynomial (g μ c)) := by
   unfold Finsupp.sum; ext
   simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
@@ -124,7 +124,7 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m)
     MvPolynomial.rename f (fromCMvPolynomial p) := by
   -- Express rename as a `Finsupp.sum` via `foldl_eq_sum`
   have step1 : CMvPolynomial.rename f p =
-      Finsupp.sum (fromCMvPolynomial p) (fun μ c =>
+      Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial p)) (fun μ c =>
         CMvPolynomial.monomial
           (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by
     show Std.ExtTreeMap.foldl

CompPoly/ToMathlib/MvPolynomial/Equiv.lean

@@ -150,16 +150,13 @@ variable. -/
 theorem support_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) :
     (finSuccEquivNth R p f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m p) f.support := by
   ext i
-  rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]
+  simp only [Polynomial.mem_support_iff, ne_eq, MvPolynomial.ext_iff, coeff_zero, not_forall,
+    Finset.mem_image, mem_support_iff, finSuccEquivNth_coeff_coeff]
   constructor
   · rintro ⟨m, hm⟩
-    refine ⟨m.insertNth p i, ?_, insertNth_apply_same _ _ _⟩
-    rw [← support_coeff_finSuccEquivNth]
-    simpa [mem_support_iff, coeff] using hm
+    exact ⟨m.insertNth p i, hm, insertNth_apply_same _ _ _⟩
   · rintro ⟨m, h, rfl⟩
-    refine ⟨m.removeNth p, ?_⟩
-    rwa [← coeff, zero_apply, ← mem_support_iff, support_coeff_finSuccEquivNth,
-      insertNth_self_removeNth]
+    exact ⟨m.removeNth p, by simpa using h⟩
 
 theorem mem_support_finSuccEquivNth {f : MvPolynomial (Fin (n + 1)) R} {x} :
     x ∈ (finSuccEquivNth R p f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m p) '' f.support := by

CompPoly/ToMathlib/Polynomial/BivariateDegree.lean

@@ -436,7 +436,8 @@ theorem degreeX_mul [IsDomain F] (f g : F[X][Y]) (hf : f ≠ 0) (hg : g ≠ 0) :
 
 /-- The evaluation at a point of a bivariate polynomial in the first variable `X`. -/
 def evalX (a : F) (f : F[X][Y]) : Polynomial F :=
-  ⟨Finsupp.mapRange (Polynomial.eval a) eval_zero f.toFinsupp⟩
+  ⟨AddMonoidAlgebra.ofCoeff
+    (Finsupp.mapRange (Polynomial.eval a) eval_zero f.toFinsupp.coeff)⟩
 
 /-- The evaluation at a point of a bivariate polynomial in the second variable `Y`. -/
 def evalY (a : F) (f : F[X][Y]) : Polynomial F :=

CompPoly/Univariate/CMvEquiv.lean

@@ -63,6 +63,8 @@ private lemma mvToUnivariate_eq_map_finSuccEquiv [CommSemiring R]
     · intro r
       simp [MvPolynomial.finSuccEquiv_apply, Polynomial.map_C,
             MvPolynomial.isEmptyRingEquiv]
+      change r = MvPolynomial.coeff (0 : Fin 0 →₀ ℕ) (MvPolynomial.C r)
+      simp [MvPolynomial.coeff_C]
     · intro i
       have hi : i = 0 := Subsingleton.elim _ _
       subst hi

CompPoly/Univariate/DivisionCorrectness.lean

@@ -407,6 +407,7 @@ private lemma raw_toPoly_degree_lt_of_size_lt (p q : Raw R)
   have hp : p.size ≤ m := by omega
   simp [Raw.coeff, hp]
 
+set_option maxHeartbeats 10000000 in
 private theorem raw_divModByMonicAux_go_spec (q : Raw R)
     (hqtrim : q.trim = q) (hqmonic : q.leadingCoeff = 1) (hqpos : 0 < q.size)
     (hqdegree : q.toPoly.degree = ((q.size - 1 : Nat) : WithBot Nat)) :
@@ -435,7 +436,7 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R)
         · rw [Raw.toPoly_zero]
           ring
         · exact raw_toPoly_degree_lt_of_size_lt p q hsize hqdegree
-      · simp [hsize]
+      · simp only [hsize, ↓reduceIte]
         let step := (p - Raw.C p.leadingCoeff * (q * Raw.X ^ (p.size - q.size))).trim
         have hstep_size : step.size < p.size := by
           exact div_step_size_lt p q hptrim hqtrim hqmonic hsize hqpos
@@ -444,20 +445,28 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R)
         have hstep_fuel : step.size ≤ fuel := by omega
         have ihstep := ih step hstep_trim hstep_fuel
         rcases ihstep with ⟨hrel, hdeg⟩
+        have hrel' := hrel
+        dsimp only [step] at hrel'
+        change
+          (Raw.divModByMonicAux.go fuel
+              (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly +
+            q.toPoly *
+              (Raw.divModByMonicAux.go fuel
+                (p - Raw.C p.leadingCoeff *
+                (q * Raw.pow Raw.X (p.size - q.size))).trim q).1.toPoly =
+            (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim.toPoly at hrel'
         constructor
-        · change
-            (Raw.divModByMonicAux.go fuel step q).2.toPoly +
-                q.toPoly *
-                  ((Raw.divModByMonicAux.go fuel step q).1 +
-                    Raw.C p.leadingCoeff * Raw.X ^ (p.size - q.size)).toPoly =
-              p.toPoly
-          rw [Raw.toPoly_add, _root_.mul_add, ← _root_.add_assoc, hrel]
-          dsimp only [step]
+        · rw [Raw.toPoly_add, _root_.mul_add, ← _root_.add_assoc, hrel']
           rw [Raw.toPoly_trim, Raw.toPoly_sub, Raw.toPoly_mul, Raw.toPoly_C,
             Raw.toPoly_mul, Raw.toPoly_pow, Raw.toPoly_X]
           rw [Raw.toPoly_mul, Raw.toPoly_C, Raw.toPoly_pow, Raw.toPoly_X]
           ring
-        · exact hdeg
+        · change
+            (Raw.divModByMonicAux.go fuel
+              (p - Raw.C p.leadingCoeff *
+              (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly.degree <
+              q.toPoly.degree at hdeg
+          exact hdeg
 
 private theorem raw_divModByMonicAux_toPoly_eq (p q : CPolynomial R)
     (hq_monic : q.toPoly.Monic) :