feat: bump lean version to 4.29.0

CompPoly/Bivariate/ToPoly.lean

@@ -50,7 +50,7 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Semiring R]
   `toImpl` and trimming, then builds the canonical bivariate sum.
   -/
 def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
-    [DecidableEq R] (p : R[X][Y]) : CBivariate R :=
+    [DecidableEq R] [Semiring (Polynomial R)] (p : R[X][Y]) : CBivariate R :=
   (p.support).sum (fun j ↦
     let cj := p.coeff j
     CPolynomial.monomial j ⟨cj.toImpl, CPolynomial.Raw.isCanonical_toImpl cj⟩)
@@ -171,9 +171,10 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
               (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ]
           · rw [ ← Finset.sum_add_distrib ]
             refine' Finset.sum_congr rfl fun x hx ↦ _
-            rw [ ← CPolynomial.monomial_add ]
-            congr
-            exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x))
+            erw [ ← CPolynomial.monomial_add ]
+            congr 1
+            apply Subtype.ext
+            exact (toImpl_add (p.coeff x) (q.coeff x)).symm
           · aesop
           · aesop
         · aesop
@@ -195,7 +196,8 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring
         unfold CBivariate.ofPoly
         induction' p.support using Finset.induction with j s hj ih
         · exact CPolynomial.eq_iff_coeff.mpr (congrFun rfl)
-        · rw [ Finset.sum_insert hj, CPolynomial.coeff_add, ih, Finset.sum_insert hj ]
+        · rw [Finset.sum_insert hj]
+          erw [CPolynomial.coeff_add, ih, Finset.sum_insert hj]
       rw [ h_coeff_sum, Finset.sum_eq_single n ]
       · rw [ CPolynomial.coeff_monomial ]
         simp +decide [ CPolynomial.toPoly ]
@@ -237,7 +239,8 @@ theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     toPoly (p * q) = toPoly p * toPoly q := by
       have h_mul : (p * q).toPoly =
           (CPolynomial.toPoly (p * q)).map (CPolynomial.ringEquiv (R := R)) := toPoly_eq_map (p * q)
-      rw [ h_mul, CPolynomial.toPoly_mul ]
+      rw [ h_mul ]
+      erw [CPolynomial.toPoly_mul]
       rw [ Polynomial.map_mul, ← toPoly_eq_map, ← toPoly_eq_map ]
 
 end ToPolyCore
@@ -310,6 +313,8 @@ 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
@@ -743,7 +748,7 @@ theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semi
       CPolynomial.coeff (swap (R := R) f) j =
         ∑ x ∈ f.supportY, CPolynomial.monomial x ((f.val.coeff x).coeff j) := by
     unfold CBivariate.swap CBivariate.supportY
-    rw [hCoeffSumOuter]
+    erw [hCoeffSumOuter]
     exact Finset.sum_congr rfl (fun x hx => hInner x)
   change CPolynomial.coeff (CPolynomial.coeff (swap (R := R) f) j) i =
     CPolynomial.coeff (CPolynomial.coeff f i) j

CompPoly/Data/Fin/BigOperators.lean

@@ -42,7 +42,7 @@ theorem div_two_pow_lt_two_pow (x i j : ℕ) (h_x_lt_2_pow_i : x < 2 ^ (i + j)):
   · simp only [h_i_eq_0, zero_add, pow_zero, Nat.lt_one_iff, Nat.div_eq_zero_iff, Nat.pow_eq_zero,
     OfNat.ofNat_ne_zero, ne_eq, false_and, false_or] at *;
     omega
-  · push_neg at h_i_eq_0
+  · push Not at h_i_eq_0
     apply Nat.div_lt_of_lt_mul (m:=x) (n:=2^j) (k:=2^i) (by
       have h_rhs_eq : 2^(i+j) = 2^j * 2^i := by
         rw [pow_add (a:=2) (m:=i) (n:=j), mul_comm]
@@ -151,7 +151,7 @@ This is useful for definitions that process elements in reverse order, like `fol
       have h := Fin.lt_last_iff_ne_last (n:=r - 1) (a:=⟨i, by omega⟩)
       simp only [Fin.last, mk_lt_mk, ne_eq, mk.injEq] at h
       have h_i_val_ne_eq: (i.val ≠ r - 1) := by
-        push_neg at h_i_eq_last
+        push Not at h_i_eq_last
         exact Fin.val_ne_of_ne h_i_eq_last
       apply Fin.mk_lt_of_lt_val
       apply h.mpr

CompPoly/Data/Nat/Bitwise.lean

@@ -35,7 +35,7 @@ lemma ENat.le_floor_NNReal_iff (x : ENat) (y : ℝ≥0) (hx_ne_top : x ≠ ⊤)
     (x : ENat) ≤ ((Nat.floor y) : ENat) ↔ x.toNat ≤ Nat.floor y := by
   lift x to ℕ using hx_ne_top
   -- y : ℝ≥0, x : ℕ, ⊢ ↑x ≤ ↑⌊y⌋₊ ↔ (↑x).toNat ≤ ⌊y⌋₊
-  simp only [Nat.cast_le, toNat_coe]
+  simp only [ENat.coe_le_coe, toNat_coe]
 
 section ENNReal
 open ENNReal
@@ -49,29 +49,11 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0}
 -- lemma ENNReal.div_lt_div_right (hc₀ : c ≠ 0) (hc : c ≠ ∞) (hab : a < b) : a / c < b / c :=
 --   (ENNReal.div_lt_div_iff_left hc₀ hc).2 hab
 
-theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
-    ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ := by
--- Let x = ↑a and y = ↑b for readability
-  let x : ENNReal := a
-  let y : ENNReal := b
-  -- Prove x and y are non-zero and finite (needed for inv_cancel)
-  have hx_ne_zero : x ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
-  have hy_ne_zero : y ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
-  have hx_ne_top : x ≠ ∞ := by exact ENNReal.natCast_ne_top a
-  have hy_ne_top : y ≠ ∞ := by exact ENNReal.natCast_ne_top b
-  have ha_NNReal_ne0 : (a : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
-  have hb_NNReal_ne0 : (b : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
-  -- (a * b)⁻¹ = b⁻¹ * a⁻¹
-  have hlhs : ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ℝ≥0)⁻¹ * (b : ℝ≥0)⁻¹) := by
-    rw [coe_inv (hr := by exact ha_NNReal_ne0)]
-    rw [coe_inv (hr := by exact hb_NNReal_ne0)]
-    rw [ENNReal.coe_natCast, ENNReal.coe_natCast]
-  have hrhs : ((a : ENNReal) * (b : ENNReal))⁻¹ = ((a : ℝ≥0) * (b : ℝ≥0))⁻¹ := by
-    rw [coe_inv (hr := (mul_ne_zero_iff_right hb_NNReal_ne0).mpr (ha_NNReal_ne0))]
-    simp only [coe_mul, coe_natCast]
-  rw [hlhs, hrhs]
-  rw [mul_inv_rev (a := (a : ℝ≥0)) (b := (b : ℝ≥0))]
-  rw [coe_mul, mul_comm]
+theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) :
+    ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ :=
+  (ENNReal.mul_inv
+    (Or.inl (Nat.cast_ne_zero.mpr ha))
+    (Or.inl (ENNReal.natCast_ne_top a))).symm
 
 lemma ENNReal.coe_le_of_NNRat {a b : ℚ≥0} : ((a : ENNReal)) ≤ (b) ↔ a ≤ b := by
   exact ENNReal.coe_le_coe.trans (by norm_cast)
@@ -367,7 +349,7 @@ lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0) :=
     simp only [Nat.and_one_is_mod, BEq.rfl, ↓reduceIte]
     rw [Nat.shiftLeft_shiftRight]
   else
-    push_neg at h_i_eq_k
+    push Not at h_i_eq_k
     simp only [beq_iff_eq, h_i_eq_k, ↓reduceIte]
     if h_k_lt_i: i < k then
       have h_res : (1 <<< i >>> k &&& 1) = 0 := by
@@ -390,7 +372,7 @@ lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0) :=
         rw [h_one_div_2_pow_k_sub_i, Nat.zero_and]
       rw [h_res]
     else
-      push_neg at h_k_lt_i
+      push Not at h_k_lt_i
       have h_res : (1 <<< i >>> k &&& 1) = 0 := by
         set i_sub_k := i - k with h_i_sub_k
         have h_i_sub_k_le_1: i_sub_k ≥ 1 := by omega
@@ -419,7 +401,7 @@ lemma and_two_pow_eq_zero_of_getBit_0 {n i : ℕ} (h_getBit : getBit i n = 0) :
     rw [getBit, h_k.symm] at h_getBit
     rw [getBit, h_getBit, Nat.zero_and]
   else
-    push_neg at h_k
+    push Not at h_k
     simp only [beq_iff_eq, h_k.symm, ↓reduceIte] at h_getBit_two_pow
     rw [getBit] at h_getBit_two_pow
     rw [getBit, getBit, h_getBit_two_pow]
@@ -448,7 +430,7 @@ lemma and_two_pow_eq_two_pow_of_getBit_eq_one {n i : ℕ} (h_getBit: getBit i n
     rw [Nat.shiftRight_and_distrib, Nat.and_assoc, Nat.and_comm (2^k >>> k) 1, ←Nat.and_assoc]
     rw [h_getBit, ←one_mul (2^k), ←Nat.shiftLeft_eq, Nat.shiftLeft_shiftRight, Nat.and_self]
   else
-    push_neg at h_k
+    push Not at h_k
     simp only [beq_iff_eq, h_k.symm, ↓reduceIte] at h_getBit_two_pow
     rw [getBit] at h_getBit_two_pow
     rw [h_getBit_two_pow, Nat.shiftRight_and_distrib, Nat.and_assoc, h_getBit_two_pow]
@@ -465,9 +447,7 @@ lemma eq_zero_or_eq_one_of_lt_two {n : ℕ} (h_lt : n < 2) : n = 0 ∨ n = 1 :=
 
 lemma div_2_form {nD2 b : ℕ} (h_b : b < 2) :
     (nD2 * 2 + b) / 2 = nD2 := by
-  rw [←add_comm, ←mul_comm]
-  rw [Nat.add_mul_div_left (x := b) (y := 2) (z := nD2) (H := by norm_num)]
-  norm_num; exact h_b;
+  omega
 
 lemma and_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2)
     (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm) :
@@ -656,7 +636,7 @@ lemma sum_eq_xor_plus_twice_and (n : Nat) : ∀ m : ℕ, n + m = (n ^^^ m) + 2 *
             rw [h_and_getBits, mul_comm (a := (n2 &&& m2)) (b := 2)];
           _ = 2 * (nVal &&& mVal) := by rw [h_and];
       rw [h_right]
-    · push_neg at h_and_getBitN_getBitM_eq_1;
+    · push Not at h_and_getBitN_getBitM_eq_1;
       have h_and_getBitN_getBitM_eq_0 : (getBitN &&& getBitM) = 0 := by
         interval_cases (getBitN &&& getBitM)
         · rfl
@@ -895,7 +875,7 @@ lemma getBit_of_sub_two_pow_of_bit_1 {n i j: ℕ} (h_getBit_eq_1: getBit i n = 1
     rw [Nat.getBit_two_pow]
     simp only [beq_iff_eq]
     simp only [h_j_eq_i, ↓reduceIte]
-    push_neg at h_j_eq_i
+    push Not at h_j_eq_i
     simp only [if_neg h_j_eq_i.symm, xor_zero]
 
 lemma getBit_of_lowBits {n: ℕ} (numLowBits : ℕ) : ∀ k, getBit k (getLowBits numLowBits n) =
@@ -915,7 +895,7 @@ lemma getBit_of_lowBits {n: ℕ} (numLowBits : ℕ) : ∀ k, getBit k (getLowBit
     · simp only [Nat.and_one_is_mod]
     · simp only [Nat.and_one_is_mod]
   else
-    push_neg at h_k
+    push Not at h_k
     have getBit_k_mask : getBit k (1 <<< numLowBits - 1) = 0:= by
       rw [Nat.shiftLeft_eq, one_mul]
       rw [getBit_of_two_pow_sub_one (i := numLowBits) (k := k)]
@@ -964,7 +944,7 @@ theorem getBit_repr {ℓ : Nat} :
       interval_cases j
       · simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod, Nat.zero_mod]
       · simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod]
-    · push_neg at h_ℓ₁
+    · push Not at h_ℓ₁
       set ℓ := ℓ₁ + 1
       have h_ℓ_eq : ℓ = ℓ₁ + 1 := by rfl
       intro j h_j
@@ -991,7 +971,7 @@ theorem getBit_repr {ℓ : Nat} :
           _ = b + 2 * m := by omega;
       have h_m : m < 2^ℓ₁ := by
         by_contra h_m_ge_2_pow_ℓ
-        push_neg at h_m_ge_2_pow_ℓ
+        push Not at h_m_ge_2_pow_ℓ
         have h_j_ge : j ≥ 2^ℓ := by
           calc _ = 2 * m + b := by rw [h_j_eq]; omega
             _ ≥ 2 * (2^ℓ₁) + b := by omega
@@ -1261,7 +1241,7 @@ lemma getBit_of_lt_two_pow {n: ℕ} (a: Fin (2^n)) (k: ℕ) :
 lemma exist_bit_diff_if_diff {n: ℕ} (a: Fin (2^n)) (b: Fin (2^n)) (h_a_ne_b: a ≠ b) :
     ∃ k: Fin n, getBit k a ≠ getBit k b := by
   by_contra h_no_diff
-  push_neg at h_no_diff
+  push Not at h_no_diff
   have h_a_eq_b: a = b := by
     apply Fin.eq_of_val_eq
     apply eq_iff_eq_all_getBits.mpr
@@ -1371,7 +1351,7 @@ lemma getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary: ∀ j
       if h_k_lt_n: k < n then
         have h_k_lt_n_add_1: k < n + 1 := by omega
         simp only [h_k_lt_n_add_1, ↓reduceDIte]
-        push_neg at h_k_eq
+        push Not at h_k_eq
         simp only [h_k_lt_n, ↓reduceDIte]
         unfold msbTerm
         interval_cases h_m_last_val: m ⟨n, by omega⟩

CompPoly/Data/Polynomial/Frobenius.lean

@@ -486,7 +486,7 @@ theorem degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X
     have h_exponent_dvd : Monoid.exponent Kˣ ∣ q ^ n - 1 :=
       Monoid.exponent_dvd_of_forall_pow_eq_one h_units_pow_eq_one
     have h_order_K : Fintype.card Kˣ = q ^ d - 1 := by
-      rw [Fintype.card_units, h_card_K]
+      erw [Fintype.card_units, h_card_K]
     have h_exp_eq_order : Monoid.exponent Kˣ = Fintype.card Kˣ := by
       rw [IsCyclic.exponent_eq_card, Nat.card_eq_fintype_card]
     rw [h_exp_eq_order, h_order_K] at h_exponent_dvd

CompPoly/Data/RingTheory/AlgebraTower.lean

@@ -42,7 +42,7 @@ variable {ι : Type*} [Preorder ι]
   {C : ι → Type*} [∀ i, CommSemiring (C i)] [AlgebraTower C]
 
 @[simp]
-def AlgebraTower.toAlgebra {i j : ι} (h : i ≤ j) : Algebra (A i) (A j) :=
+abbrev AlgebraTower.toAlgebra {i j : ι} (h : i ≤ j) : Algebra (A i) (A j) :=
   (AlgebraTower.algebraMap (i:=i) (j:=j) (h:=h)).toAlgebra
 
 @[simp]
@@ -102,11 +102,11 @@ def AlgebraTowerEquiv.algebraMapLeftUp (e : AlgebraTowerEquiv A B) (i j : ι)
   have hjRingEquiv: RingEquiv (B i) (A i) := (e.toRingEquiv i).symm
   exact hAij.comp hjRingEquiv.toRingHom
 
-def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
+abbrev AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
     (h : i ≤ j) : Algebra (A i) (B j) := by
   exact (e.algebraMapRightUp i j h).toAlgebra
 
-def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι)
+abbrev AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι)
     (h : i ≤ j) : Algebra (B i) (A j) := by
   exact (e.algebraMapLeftUp i j h).toAlgebra
 

CompPoly/Data/Vector/Basic.lean

@@ -89,7 +89,7 @@ lemma cons_empty_tail_eq_nil {α} (hd : α) (tl : Vector α 0) :
 theorem tail_cons {α} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).tail = tl := by
   rw [cons, Vector.insertIdx]
   simp only [Nat.add_one_sub_one, Array.insertIdx_zero, tail_eq_cast_extract, extract_mk,
-    Array.extract_append, List.extract_toArray, List.extract_eq_drop_take, add_tsub_cancel_right,
+    Array.extract_append, List.extract_toArray, List.extract_eq_take_drop, add_tsub_cancel_right,
     List.drop_succ_cons, List.drop_nil, List.take_nil, List.size_toArray, List.length_cons,
     List.length_nil, tsub_self, Array.take_eq_extract, Array.empty_append, cast_mk, mk_eq,
     Array.extract_eq_self_iff, size_toArray, le_refl, and_self, or_true]

CompPoly/Fields/Binary/AdditiveNTT/Algorithm.lean

@@ -100,7 +100,7 @@ lemma evaluationPointω_eq_twiddleFactor_of_div_2 (i : Fin ℓ) (x : Fin (2 ^ (
   simp only [Nat.getBit, Nat.shiftRight_zero, Nat.and_one_is_mod]
   by_cases h_lsb_of_x_eq_0 : x.val % 2 = 0
   · simp only [h_lsb_of_x_eq_0, zero_ne_one, ↓reduceIte, Nat.cast_zero, zero_mul]
-  · push_neg at h_lsb_of_x_eq_0
+  · push Not at h_lsb_of_x_eq_0
     simp only [ne_eq, Nat.mod_two_not_eq_zero] at h_lsb_of_x_eq_0
     simp only [h_lsb_of_x_eq_0, ↓reduceIte, Nat.cast_one, one_mul]
 
@@ -159,7 +159,7 @@ lemma eval_point_ω_eq_next_twiddleFactor_comp_qmap
     conv_rhs => rw [h_0_is_algebra_map]
     have h_res := qMap_eval_𝔽q_eq_0 𝔽q β (i := ⟨i, by omega⟩) (c := 0)
     rw [h_res]
-  · push_neg at h_bit_of_x_eq_0
+  · push Not at h_bit_of_x_eq_0
     have h_bit_lt_2 := Nat.getBit_lt_2 (k := x1) (n := x)
     have bit_eq_1 : Nat.getBit x1 x = 1 := by
       interval_cases Nat.getBit x1 x

CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean

@@ -277,7 +277,7 @@ lemma NTTStage_correctness (i : Fin (ℓ))
     rw [h_x0_eq_cur_evaluation_point]
     simp only [eval_comp, eval_add, eval_mul, eval_X]
   · simp only [h_b_bit_eq_0, ↓reduceDIte]
-    push_neg at h_b_bit_eq_0
+    push Not at h_b_bit_eq_0
     have bit_i_j_eq_1 : Nat.getBit i.val j.val = 1 := by omega
     simp only [ne_eq, Nat.mod_two_not_eq_zero] at h_b_bit_eq_0
     set x1 := twiddleFactor 𝔽q β h_ℓ_add_R_rate i
@@ -501,12 +501,13 @@ theorem additiveNTT_correctness (h_ℓ : ℓ ≤ r)
   have res := output_foldl_correctness j
   unfold output_foldl at res
   simp only [Fin.zero_eta, Nat.sub_zero, pow_zero, Nat.div_one, Fin.eta,
-    Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue, base_coeffsBySuffix] at res
+    Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue] at res
   simp only [←
     intermediate_poly_P_base 𝔽q β h_ℓ_add_R_rate
       h_ℓ original_coeffs,
     Fin.zero_eta]
-  rw [← res]
+  erw [base_coeffsBySuffix] at res
+  erw [← res]
   simp_rw [Nat.sub_right_comm]
 
 end AlgorithmCorrectness

CompPoly/Fields/Binary/AdditiveNTT/Impl.lean

@@ -6,6 +6,7 @@ Authors: Chung Thai Nguyen, Quang Dao
 
 import CompPoly.Fields.Binary.AdditiveNTT.Algorithm
 import CompPoly.Fields.Binary.Tower.Concrete.Basis
+import Mathlib.Data.BitVec
 
 /-!
 # Additive NTT Implementation
@@ -399,7 +400,8 @@ abbrev BTF₃ := ConcreteBTField 3 -- 8 bits
 instance : NeZero (2^3) := ⟨by norm_num⟩
 instance : Field BTF₃ := instFieldConcrete
 instance : DecidableEq BTF₃ := (inferInstance : DecidableEq (ConcreteBTField 3))
-instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3))
+instance : Fintype BTF₃ :=
+  Fintype.ofEquiv (Fin (2 ^ (2 ^ 3))) (BitVec.equivFin (m := 2 ^ 3)).symm.toEquiv
 
 /-- Test of the computable additive NTT over BTF₃ (an 8-bit binary tower field `BTF₃`).
 **Input polynomial:** p(x) = x (novel coefficients [7, 1, 0, 0]) of size `2^ℓ` in `BTF₃`

CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean

@@ -380,7 +380,7 @@ lemma getSDomainBasisCoeff_of_iteratedQuotientMap
           simp only [zero_add]
           omega⟩)
       simp only [Fin.zero_eta, Fin.coe_ofNat_eq_mod, Nat.sub_zero] at h_interW_comp
-      rw [h_interW_comp]
+      erw [h_interW_comp]
       have h_index : 0 + i.val = i.val := by omega
       rw! (castMode := .all) [h_index]
       rfl
@@ -480,7 +480,7 @@ theorem base_intermediateNovelBasisX (j : Fin (2 ^ ℓ)) :
   simp only [Fin.mk_zero'] at h_res
   conv_lhs =>
     enter [2, x, 1]
-    rw [h_res ⟨x, by omega⟩]
+    erw [h_res ⟨x, by omega⟩]
   congr
 
 omit [DecidableEq L] [DecidableEq 𝔽q] h_Fq_char_prime hF₂ hβ_lin_indep h_β₀_eq_1 in